Program States and Control Flow Interruptions

The RISC ProgramExplorer also supports the arbitrary use of the commands continue, break, return, throw that interrupt the control flow by jumping to the next loop iteration, to the command succeeding the loop, to the caller of a method, or to the handler of an exception. The specification language takes this feature into account by supporting a type STATE(T) which denotes the state before/after execution of a command inside a method that returns a value of type T (i.e., T denotes the mathematical counterpart of the corresponding program type); the type STATE denotes the corresponding type for a method of type void. In a specification, the constants NOW and NEXT are of this type; NOW denotes the pre-state of the command and NEXT denotes its post-state. Specifications may expressed with the following state functions (where s denotes a state):

The most frequently occurring term of this kind is VALUE@NEXT which describes a function’s return value.

Furthermore, we have the following state predicates (which are exhaustive and disjoint; i.e. a state is exactly in one of the denoted modes):

Finally, we have the state predicate s1~s2 which denotes that s1 and s2 (which may be of different state types) are equal up to the state’s return value.

After translation of a verification condition from state logic to classical logic, a state is represented by a record type

STATE: TYPE =
[#mode: INT, val: …, exception: INT, message: …#];

where an integer field mode holds a numerical code for the execution mode, val holds the state’s return value, exception holds a code for the exception’s type, and message holds the exception’s message. The state functions above are translated to corresponding functions value_ and message_ that extract the corresponding information from the record. The state predicates above are translated to corresponding predicates executes_, continues_, breaks_, returns_, throws_, and throwsException_ that test the record’s mode field.

As a simple example, take the following method isSorted which returns TRUE if and only if a given integer array is sorted in ascending order:

/*@
theory uses Base {
  int: TYPE = Base.int;
  intArray: TYPE = Base.IntArray;
  isSorted: PREDICATE(intArray, int) =
    PRED(a: intArray, n: int):
      FORALL(i: INT): 1 <= i AND i < n =>
        a.value[i-1] <= a.value[i];
}
@*/
class Arrays
{
  public static boolean isSorted(int[] a) /*@
    requires (VAR a).null = FALSE;
    ensures (VALUE@NEXT=TRUE) <=>
            isSorted(VAR a, (VAR a).length);
  @*/
  {
    int n = a.length;
    for (int i=1; i<n; i++)
    /*@ invariant …; decreases …; @*/
   {
      if (a[i-1] > a[i]) return false;
   }
    return true;
  }
}

The program loop is adequately specified by the following invariant and termination term:

invariant (VAR a).null = FALSE AND VAR n = (VAR a).length
  AND 1 <= VAR i AND (VAR n >= 1 => VAR i <= VAR n)
  AND (EXECUTES@NEXT => isSorted(VAR a, VAR i))
  AND (RETURNS@NEXT =>
         VALUE@NEXT = FALSE AND
         VAR i < VAR n AND
         (VAR a).value[VAR i-1] > (VAR a).value[VAR i]);
decreases VAR n - VAR i + 1;

The invariant says that, if the loop is still executing, the array is know to be sorted up to position i; if the loop, however, executes the return statement, it is with a return value false because at position i the order is violated.

If we switch to the “Semantics” view of the method, we can consequently investigate the semantics of return false (which as seen by the effects always returns)

The state relation shows that there exist two cases in the second case, the return value is “false” because a violation in the sorting order has been detected at position in; in the first case (whose description could be considerably simplified because executes@state₁ and returns@state₁ are incompatible), the result is “true” and the array is sorted up to position in = n = old a.length.

For method isSorted the usual verification tasks are generated where only the proof of the postcondition, the loop precondition, the preservation of the loop invariant, and the decrement of the loop measure require human guidance. For instance, the postcondition proof

requires the expansion of the predicate isSorted and the heuristic instantiation of the resulting universal formula. The proof of the loop precondition (the loop invariant hold initially)

requires the expansion of auxiliary predicates “executes_” and “returns_” (which represent in the RISC ProofNavigator the corresponding state predicates mentioned above) to show that they cannot hold for the same state. The other proofs proceed in a similar fashion.

4.4 Program States and Control Flow Interruptions