Better

Author: leavens

tutorial/exercises/Animal2.java

@@ -19,6 +19,6 @@ public Animal2(String g)
 
     public void setAge(int a) {
         if (a < _age) { return; }
-        if (_age <= a && a <= 150) { _age = a; }
+        _age = a;
     }
 }

tutorial/exercises/ExceptionalSetAge2.java

@@ -3,6 +3,6 @@ public interface ExceptionalSetAge2 extends Age {
     /*@ normal_behavior
       @   requires a < age;
       @   assignable \nothing;
-      @   ensures \old(age) == age; @*/
+      @*/
     void setAge(int a); 
 }

tutorial/exercises/InheritingSpecificationsEx.md

@@ -74,14 +74,13 @@ c. **If the inherited implementations of the methods `setX` and `setY` are not c
 ```
 
 ## **Question 3**
-**Specify another interface, called `ExceptionalSetAge`, that also includes a new method `setAge` (new compared to `Age`, that is). The interface `ExceptionalSetAge` must extend the interface `Age` shown above. The added `setAge` method should take an integer that is (strictly) less than the value of `age` and throw an `IllegalArgumentException`. When this happens, the method should not assign to any variables.
-However, so that further exercises may involve classes that extend both `NormalSetAge` and this interface (`ExceptionalSetAge`) and which can assign to additional fields, it is necessary to allow the inherited model field `age` to be assigned by the `setAge` method.  So think about what postcondition would specify the appropriate behavior.**
+**Specify another interface, called `ExceptionalSetAge`, that also includes a new method `setAge` (new compared to `Age`, that is). The interface `ExceptionalSetAge` must extend the interface `Age` shown above. The added `setAge` method should take an integer that is (strictly) less than the value of `age` and throw an `IllegalArgumentException`. When this happens, the method should not assign to any variables.**
 
 ## **Question 4**
-**Specify an interface, called `Gendered` that includes a model instance field `gender` of type `String`. Your task is to write this interface's specification and to specify a Boolean-valued `spec_pure` method named `isFemale()` that returns `true` just when the receiver (an object of a subtype of `Gendered`) is has the gender female.**
+**Specify an interface, called `Gendered` that includes a model instance field `gender` of type `String`. Your task is to write this interface's specification and to specify a Boolean-valued `spec_pure` method named `isFemale()` that returns `true` just when the receiver (an object of a subtype of `Gendered`) is has the gender value `"female"`.**
 
 ## **Question 5**
-**Specify and correctly implement a class, call it `Animal` that implements the interfaces `Gendered`, `NormalSetAge`, and `ExceptionalSetAge`. You will need to implement a constructor that takes a `String` argument that determines the gender of the new object, but starts the age at 0. You may assume that animals are either male or female. Hints: think about the precondition of the constructor. Use a protected field `_gen` to represent the model field `gender` that is inherited from the (specification of the) interface `Gendered`. Note that each model field names a datagroup, and when a concrete field is used to represent that datagroup, then it must be added into that datagroup using an `in` annotation in JML. Being in a datagroup allows the representing field to be assigned when the datagroup is allowed to be assigned by the specification. Similarly, add a protected model field `_age` that is used to represent the inherited model field `age`. Making these concrete fields protected allows them to be inherited by subclasses of Animal. Since they are protected, the represents clauses that are used must also be protected. [See the lesson on model fields and datagroups](https://www.openjml.org/tutorial/ModelFields) for more about represents clauses.**
+**Specify and correctly implement a class, call it `Animal` that implements all three interfaces `Gendered`, `NormalSetAge`, and `ExceptionalSetAge`. You will need to implement a constructor that takes a `String` argument that determines the gender of the new object, but starts the age at 0. You may assume that animals are either male or female. Hints: think about the precondition of the constructor. Use a protected field `_gen` to represent the model field `gender` that is inherited from the (specification of the) interface `Gendered`. Note that each model field names a datagroup, and when a concrete field is used to represent that datagroup, then it must be added into that datagroup using an `in` annotation in JML. Being in a datagroup allows the representing field to be assigned when the datagroup is allowed to be assigned by the specification case's frame condition. Similarly, use a protected model field `_age` to represent the inherited model field `age`. Making these concrete fields protected allows them to be inherited by subclasses of `Animal`. Since they are protected, the represents clauses that are used must also be protected. [See the lesson on model fields and datagroups](https://www.openjml.org/tutorial/ModelFields) for more about represents clauses.**
 
 ## **Question 6**
 **Specify and implement a class `Human` as a subclass of `Animal`. A `Human` should have a Boolean-valued public model field `discount` that is represented by some protected concrete (instance) field. The `setAge` method should have an additional specification case that makes `discount` be `true` when the age used as an argument to `setAge` is 65 or greater. Hint: use a call to `super` in your implementation of `setAge`.**
@@ -92,8 +91,11 @@ However, so that further exercises may involve classes that extend both `NormalS
 ## **Question 8**
 **Specify an `equals` method for the interface `Gendered`. Then correctly implement it in the class `Animal`. Make sure that two Animals (or Humans or Tortoises) with different ages are not equal, even if they have the same gender.**
 
+## Advanced Exercises
+The following two exercises delve into deeper aspects of specification inheritance and can be skipped on first reading.
+
 ## **Question 9**
-**Specify a version of the interface `ExceptionalSetAge`, call it `ExceptionalSetAge2` that instead of throwing an exception when the arugment is strictly less than `age`, the `setAge` method should not assign to anything.**
+**Specify a version of the interface `ExceptionalSetAge`, call it `ExceptionalSetAge2` that instead of throwing an exception when the argument is strictly less than `age`, the `setAge` method should have a normal behavior that returns without assigning anything.**
 
 ## **Question 10**
 **Specify and correctly implement versions of the classes `Animal` and `Human` that inherit from `ExceptionalSetAge2`.

tutorial/exercises/InheritingSpecificationsExKey.md

@@ -150,7 +150,7 @@ This exercise shows that preconditions can be further weakened in a subtype, as
 Note that the method setAge cannot simply be inherited, because the precondition of the method `setAge` in the class `Animal` has a different precondition, and that precondition must be weakened in the implementation in `Tortoise`.
 
 ## **Question 8**
-One way to specify an interface like `Gendered` but with an `equals` method that allows for other attributes (aside from the gender) to be taken into account is to say that when the genders are differnt, then the `equals` method must return false. This has the advantage of allowing other attributes of an object to be considered, while requiring comparison of the genders.  This is shown in the following.
+One way to specify an interface like `Gendered` but with an `equals` method that allows for other attributes (aside from the gender) to be taken into account is to say that when the genders are different, then the `equals` method must return false. This has the advantage of allowing other attributes of an object to be considered, while requiring comparison of the genders.  This is shown in the following.
 
 ```
 public interface GenderedWithEquals {
@@ -174,6 +174,8 @@ However, this cannot be strengthened to say that when the genders are equal, the
 
 Also recall that Java's `instanceof` operator returns false if its left-hand argument is null. Thus, when `obj instanceof GenderedWithEquals` is true, we know that `obj` must not be null, and so a cast will work.
 
+## Advanced Exercises
+
 ## **Question 9**
 One solution is the following.
 
@@ -182,13 +184,15 @@ public interface ExceptionalSetAge2 extends Age {
     /*@ normal_behavior
       @   requires a < age;
       @   assignable \nothing;
-      @   ensures \old(age) == age; @*/
+      @*/
     void setAge(int a); 
 }
 ```
 
+Sine this behavior specification is in an interface, it has public visibility and thus does not need to be use the modifier `public`.  It would be possible to specify a postcondition (for example `age == \old(age)` would work), but the default of `true` suffices in this case, because of the specified frame. However, one should not specify the method as `pure`, because `pure` applies to the entire method and not just one specification case.
+
 ## **Question 10**
-A class that is similar to `Animal`, called `Animal2` below, inherits from the aabove interface `ExceptionalSetAge2`. Notice that in the implementation of `setAge` obeys both specifications of the method `setAge`.
+A class that is similar to `Animal`, called `Animal2` below, inherits from the above interface `ExceptionalSetAge2`. Notice that in the implementation of `setAge` obeys both specifications of the method `setAge`.
 
 ```
 public class Animal2 implements Gendered,
@@ -211,7 +215,7 @@ public class Animal2 implements Gendered,
 
     public void setAge(int a) {
         if (a < _age) { return; }
-        if (_age <= a && a <= 150) { _age = a; }
+        _age = a;
     }
 }
 
@@ -240,3 +244,5 @@ public class Human2 extends Animal2 {
     }
 }
 ```
+
+Notice that the implementation of `setAge` in `Human2` cannot just make a super call, as such a call `super.setAge(a)` would simply return to the code of `setAge` in `Human2`, whereas in the class `Human` that call would throw an exception. It is thus necessary to prevent an assignment to `_discount` (which is in the datagroup `age`) by returning when the argument `a` is strictly less than `_age`.