[prev] [prev-tail] [tail] [up]

4.5  Objects and Method Side Effects

The RISC ProgramExplorer also supports reasoning over objects as shown in the following implementation of the abstract datatype “stack”:


public class Stack2 /*@
  invariant
    (VAR stack).null = FALSE AND
    0 <= VAR n AND VAR n <= (VAR stack).length;
@*/
{
  private int[] stack;
  private int n;

  public Stack2() /*@
    assignable this;
    ensures VAR n = 0;
  @*/
  {
    stack = new int[10];
    n = 0;
  }

  public boolean isEmpty() /*@
    ensures VALUE@NEXT = TRUE <=> VAR n = 0;
  @*/
  {
    return n == 0;
  }

  public int top() /*@
    requires VAR n > 0;
    ensures  VALUE@NEXT = (VAR stack).value[VAR n-1];
  @*/
  {
    return stack[n-1];
  }

  public int pop() /*@
    requires VAR n > 0;
    assignable n;
    ensures VALUE@NEXT = (VAR stack).value[OLD n-1]
        AND VAR n = OLD n-1;
  @*/
  {
    int result = top();
    n = n-1;
    return result;
  }

  public void push(int v) /*@
    requires (VAR n = (VAR stack).length =>
               2*(VAR stack).length+1 <= Base.MAX_INT);
    assignable stack, n;
    ensures VAR n = OLD n+1


        AND (VAR stack).value[OLD n] = VAR v;
  @*/
  {
    if (n == stack.length)
      stack = resize();
    stack[n] = v;
    n = n+1;
  }

  private int[] resize() /*@
    helper;
    requires
      (VAR stack).null = FALSE AND
      0 <= VAR n AND VAR n <= (VAR stack).length AND
      2*(VAR stack).length+1 <= Base.MAX_INT;
    ensures LET result = VALUE@NEXT IN
      result.null = FALSE AND
      result.length > (OLD stack).length AND
      (FORALL(i: INT): 0 <= i AND i < VAR n =>
         result.value[i] = (OLD stack).value[i]);
  @*/
  {
    int[] stack0 = new int[2*stack.length+1];
    for (int i=0; i<n; i++) /*@
      invariant
        (VAR stack).null = FALSE AND
        0 <= VAR n AND VAR n <= (VAR stack).length AND
        0 <= VAR i AND VAR i <= VAR n AND
        (VAR stack0).null = FALSE AND
        (VAR stack0).length > (OLD stack).length AND
        (FORALL(i: INT): 0 <= i AND i < VAR i =>
           (VAR stack0).value[i] = (OLD stack).value[i]);
      decreases VAR n - VAR i;
    @*/
      stack0[i] = stack[i];
    return stack0;
  }
}

The main features of this program are the following:

  1. The invariant in the class header specifies an object invariant, i.e. a state condition
    1. that is added to the postcondition of every constructor and object method,
    2. that is added to the precondition of every object method (not constructor)

    provided the method is not tagged as helper (as is the auxiliary method resize() above5

  2. The assignable clauses in the method headers constrain the side effects of the method by indicating which globally visible variables may be changed by the execution of the method. A specification assignable this indicates that every variable in the current object may be changed; a specification of assignable var (with object variable var) specifies that only the variable var in the current object may be changed (all other variables in the current object remain the same); a specification assignable object.var specifies that in object object only the variable var may be changed.

    Similar specifications are allowed for class variables (in the current class or other classes using the syntax assignable class.var). If no assignable clause is given, the method is “pure”, i.e., does not change any object or class variable.

An object of type Stack2 is represented by the following record type (defined in the automatically generated theory Stack2):


Stack2: TYPE =
  [#stack:
     [#value: ARRAY Base.int OF Base.int,
       length: Base.nat, null: BOOLEAN#],
    n: Base.int, null: BOOLEAN, new: INT#]

The record type contains one field for every object variable as well as the automatically generated fields null (if set to TRUE, the record represents the null value) and new (set to an unknown value after the construction of the object; the results of two constructor calls are thus never equal). The specification variable this is a value of this type.

Based on this representation, the semantics of the object method push is as follows:

Push Method

We see that the effect of the method is a modification of the value of this (of record type Stack2); if some object variables are not changed, a corresponding equality is provided as part of the transition relation.

For each of the object methods, as usual a couple of tasks are generated; however, most of them can be solved automatically by the validity checker or the scatter strategy. Also the remaining interactive proofs are very simple and require only minor human guidance.

[prev] [prev-tail] [front] [up]