Use old defined g several times

Author: leavens

tutorial/OldAndOrdering.md

@@ -29,15 +29,15 @@ Some of these have been already discussed; others are discussed in later lessons
 There is no pre-defined order to the clauses within a single specification case (cf. a later lesson on [multiple specification cases](MultipleBehaviors)].
 However, a specification is much more readable if the clauses generally follow the order above, with preconditions first, then frame conditions, followed by postconditions.
 
-There is some meaning to the ordering within the precondition group and within the postcondition group: earlier clauses can set conditions that are needed for later clauses to be well-defined; but ordering only matters within the kinds of precondition clauses and separately for any `ensures` clauses. For example,
+There is some meaning to the ordering within the precondition group and within the postcondition group: earlier clauses can set conditions that are needed for later clauses to be well-defined; but ordering only matters within the each kinds of clause; that is ordering matters within the set of precondition clauses and separately for any `ensures` clauses. For example,
 ```
 {% include_relative T_order1.java %}
 ```
 yields
 ```
 {% include_relative T_order1.out %}
 ```
-The first requires clause might not be well-defined because `a` might be null. If we reverse the order of the clauses, then OpenJML is content:
+The first requires clause might not be well-defined because `a` might be null. If we reverse the order of the clauses, as in the following specification, then the method verifies:
 ```
 {% include_relative T_order2.java %}
 ```

tutorial/T_Old.java

@@ -3,9 +3,20 @@ public class T_Old {
 
   //@ requires x > 0 && y > 0;
   //@ old \bigint g = Math.gcd(x,y); // spec from Math library
-  //@ ensures \result == g;
+  //@ requires g+g+g <= Integer.MAX_VALUE;
+  //@ ensures \result == g+g+g;
   public int myGCD(int x, int y) {
      // some code
-     return 0; // placeholder
+     int g = mygcd(x,y);
+     return g+g+g;
+  }
+
+  //@ requires x > 0 && y > 0;
+  //@ old \bigint g = Math.gcd(x,y); // spec from Math library
+  //@ requires g+g+g <= Integer.MAX_VALUE;
+  //@ ensures \result == Math.gcd(x,y); // spec from Math library
+  //@ pure
+  public int mygcd(int x, int y) {
+      return 0; // placeholder
   }
 }