4.3  Searching in Arrays

Our next example discusses the semantics and verification of a method search which implements linear search of a given integer array a for a key x; the method returns the smallest position of an occurrence of x in a, respectively -1, if x does not occur in a.


public class Searching
{
  public static int search(int[] a, int x) /*@
    requires …;
    ensures …;
  @*/
  {
    int n = a.length;
    int r = -1;
    int i = 0;
    while (i < n && r == -1) /*@
      invariant …;
      decreases …;
    @*/
    {
      if (a[i] == x)
        r = i;
      else
        i = i+1;
    }
    return r;
  }
}

The specification of the method is as follows:


requires (VAR a).null = FALSE;
ensures
  LET result = VALUE@NEXT, n = (VAR a).length IN
    IF result = -1 THEN
      FORALL(i: INT): 0 <= i AND i < n =>
        (VAR a).value[i] /= VAR x
    ELSE
      0 <= result AND result < n AND
      (FORALL(i: INT): 0 <= i AND i < result =>
        (VAR a).value[i] /= VAR x) AND
        (VAR a).value[result] = VAR x
    ENDIF;

The program array a is represented by a mathematical variable var a with the following type IntArray (declared in theory Base):


int: TYPE = [MIN_INT..MAX_INT];
nat: TYPE = [0..MAX_INT];
IntArray: TYPE =
  [#value: ARRAY int OF int, length: nat, null: BOOLEAN#];

The precondition states that a must not be the null pointer. The postcondition describes the two possible method results using the terms var a.length to refer to the number of elements in a and var a.value[i] to refer to the value at position i.

The loop is correspondingly annotated with the following invariant and termination term:


invariant (VAR a).null = FALSE AND VAR n = (VAR a).length
      AND 0 <= VAR i AND VAR i <= VAR n
      AND (FORALL(i: INT): 0 <= i AND i < VAR i =>
             (VAR a).value[i] /= VAR x)
      AND (VAR r = -1 OR (VAR r = VAR i AND VAR i < VAR n AND
             (VAR a).value[VAR r] = VAR x));
decreases IF VAR r = -1 THEN VAR n - VAR i ELSE 0 ENDIF;

The termination term is defined by two cases, since if x is found in a, i is not incremented but r is set to -1.

From the specified method, the following information is displayed in the “Semantics” view of method linsearch:

Linear Search Semantics

We see that the body is executed in a state when a is not null and that the termination condition is ensured since the length of a is always non-negative; from the transition relation, we can deduce that up to a certain position 0 in old a.length (the value of i at the termination of fac) the key x does not occur in a and that one of the two cases occurs:

  1. the return value is -1 and in = n, or
  2. the return value equals in and a holds x at that position.

From this the partial correctness of the method is pretty self-evident.

The semantics of the while loop is depicted as follows:

Linear Search Semantics

In the pre-state knowledge, we can derive the values of n, r, and i when the loop starts execution. From the effect clause, we can deduce that the loop is only terminated by the loop expression and that the only modified variables are r and i. The transition relation gives essentially the same information as for the method body discussed above. The termination condition states that the termination term must be initially non-negative; from the pre-state knowledge, we know that this is the case because n equals the length of a and i is 0.

The semantics of the loop body is depicted as follows:

Linear Search Semantics

We see that only the variables r and i are modified as described by the transition relation. The semantics of the body statement i=i+1

Linear Search Semantics

has a precondition that restricts the value of old i+1 to the domain of type int; fortunately this can be established from the pre-state knowledge old i 0 and old i < old n = old a.length.

The “Analysis” view depicts the following (non-trivial) verification tasks:

Linear Search Tasks

We see that the verification of the method’s effects, its termination, and that the loop measure is well-formed and decreased by every iteration have been performed automatically by the validity checker. The verification of the individual preconditions can be performed by the automatic scatter strategy respectively built-in simplification of the RISC ProofNavigator. The only two tasks that require interactive proofs are related to the method’s partial correctness and the preservation of the invariant.

The verification of partial correctness amounts to proving that the method’s state relation depicted above implies the post-condition; the corresponding proof proceeds with minor help:

Linear Search Postcondition

Also the verification of the loop invariant requires only minor guidance to split the goal appropriately towards those two proof branches that can be solved by heuristic instantiation:

Linear Search Invariant

We see that with slightly more aggressive automation of proof search, also these proofs could have been performed fully automatically.