Method Calls in Specifications

June 22, 2010 – 6 years, 9 months ago, by eifler

Short Description

Develop a specification and verification technique that allows one to determine the effects of heap modifications on the results of observer methods.

Code

public interface BoundedStack {
   /*@ pure @*/ boolean hasRoomFor(int i);

   //@ requires hasRoomFor(1);
   //@ assignable this.*;
   void push(int i);
   /* other methods omitted */
}

public class Calculator {
   /*@ spec_public @*/ BoundedStack stack;
   int[] operands;
   int next;
   
   //@ requires stack.hasRoomFor(1);
   public void constOp() {
      int op = getOperand();
      stack.push(op);
   }
   //@ assignable next;
   int getOperand() {
      int res = operands[next];
      next++;
      return res;
   }
   /* other class members omitted */
}

Interface BoundedStack uses the pure method hasRoomFor to provide an implementation-independent JML specification for push. The notation this.* in push’s assignable clause means that all fields of this (including the inherited model field objectState and its data group) are assignable. Class Calculator uses a BoundedStack to store a stack of operands. The method constOp fetches an operand and pushes it onto the stack. The modifier spec_public allows the field stack to be used in public specifications.

public class StrangeStack implements BoundedStack {
   Calculator calc;
   int count;

   /*@ pure @*/ public boolean hasRoomFor(int i) {
     return i <= calc.next - count;
   }
}

A possible implementation of interface BoundedStack. The stack elements are stored in the unused part of the operand array of the Calculator object calc. Consequently, modifications of calc.next affect the capacity of the stack and, therefore, the result of hasRoomFor.

Specification

Long Description

Assertions in Eiffel, JML, and Spec# rely on pure (that is, side-effect free) methods, so-called observers, to support data abstraction. For instance, the BoundedStack interface in the code example above contains an observer method hasRoomFor, where stack.hasRoomFor(i) yields true if and only if stack has room for at least i additional elements. This observer is used to provide a specification for method push without referring to the concrete implementation of the stack. Implementation independence is required by information hiding. Moreover, implementation independence is crucial to supporting subtyping since different subtypes must satisfy a common specification, but may have different implementations (or no implementations at all in the case of abstract classes and interfaces).
Recent papers by Cok as well as by Darvas and Müller present encodings of observer methods in program logics. However, they do not explain how to reason about frame properties when the specification uses observer methods.
Existing specification techniques for frame properties [LBR06, LM06, LN02, MPHL03] allow one to describe the fields that are potentially modified by a method execution using an assignable clause. However, assignable clauses do not specify the effects of a method execution on the results of observers. In our example, method push affects the result of hasRoomFor for some arguments, but this effect is not declared in push’s assignable clause.
Since effects on observers are not covered by assignable clauses, the specification of method getOperand of class Calculator does not express whether the result of stack.hasRoomFor is potentially affected by the method. In fact, the specification in Fig. 5 does not prevent such an interaction between getOperand and
stack.hasRoomFor. Class StrangeStack stores the stack elements in the unused part of the operand array of the Calculator object calc. Consequently, modifications of calc.next affect the capacity of the stack and, therefore, the result of hasRoomFor. If a Calculator object c and a StrangeStack object mutually use each other, then calling c.getOperand may indeed affect the result of c.stack.hasRoomFor.
Due to its requires clause, method constOp may assume stack.hasRoomFor(1). However, we cannot conclude that this property still holds when it is needed to satisfy the requires clause of the call to stack.push, because that property might have been invalidated by the preceding call to getOperand. Consequently, we cannot prove that the requires clause of push is satisfied, which causes the verification of constOp to fail. This example illustrates the challenge.

Supplementary Materials

The paper by Gary T. Leavens and K. Rustan M. Leino and Peter Müller from which this challenge is taken contains some additional information including references to relevant papers related to this challenge. Some more specification and verification challenges which are also included on this site can also be found there.

Submitted by

Timo Eifler verifythis@cost-ic0701.org