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

3.2  Searching for Records

This example deals with the specification of a program that searches in an array of records for a record with a specific key. The example is based on the following program class:


class Record
{
  String key;
  int value;

  Record(String k, int v)
  {
    key = k;
    value = v;
  }

  boolean equals(String k)
  {
    boolean e = key.equals(k);
    return e;
  }

  public static int search(Record[] a, String key)
  {
    int n = a.length;
    for (int i=0; i<n; i++)
    {
      Record r = new Record(a[i].key, a[i].value);
      boolean e = r.equals(key);
      if (e) return i;
    }
    return -1;
  }

  public static void main()
  {
    int N = 10;
    Record[] a = new Record[N];
    for (int i=0; i<N; i++)
      a[i] = new Record(~abc~, i);
    a[5] = new Record(~xyz~, 5);
    int i = search(a, ~xyz~);
    System.out.println(i);
  }
}

This program introduces an object type Record with a string field key and an integer field value. The type has an constructor to build a record from an given string and integer and a method equals that allows to check whether the record has the denoted key. This function calls the method equals on object type String; while this class is part of the Java standard library, it has to be explicitly defined in a file accessible to the RISC ProgramExplorer. We therefore introduce a dummy class


package java.lang;
public class String
{
  public boolean equals(String s)  return false; 
}
solely for declaring the method equals (without caring for the actual representation of strings or the actual implementation of the method). Unlike real Java, our programming language only allows to call program methods with return values to initialize/assign to variables, not as parts of program expressions1 . The two statements


  boolean e = key.equals(k);
  return e;

in the body of equals can therefore not be merged into one.

The core of the program is the method search which takes an array a of records and a key and returns the index of the first record in a that contains that key (or -1, if there is no such record). The core of the method body is represented by the two statements


  Record r = new Record(a[i].key, a[i].value);
  boolean e = r.equals(key);

The first statement builds a record r from the key and the value of record a[i]. The second statement calls the method equals on r to compare its key with key. This apparently clumsy way of using the function equals is necessary because the specification formalism considers object variables (variables of object types) to hold object values rather than object references (which considerably simplifies reasoning because then the modification of an object via one variable cannot affect an object referenced by another variable).

However, since the programming language Java (like most programming languages) lets object variables hold references, the semantics of our programming language would deviate from classical program semantics. Therefore the type checker ensures that two different program variables cannot refer to the same object; consequently it does not make any difference whether an object variable holds an object value or an object reference. Consequently, if equals would modify its record, above solution would not update array a (independent of whether object variables hold object values or object references) while the solution


  Record r = a[i];
  boolean e = r.equals(key);

would update a in a language with reference semantics for objects but not in a language with value semantics. For similar reasons, the even shorter solution


  boolean e = a[i].equals(key);

is also (even syntactically) prohibited. See Appendix B for a more thorough description of the constraints of our programming language compared to Java.

The method main of the program creates an array, fills it with values, updates it, and calls the method search in the usual way. It also calls the method System.out.println of the Java Standard API. This method has to be declared with the help of the dummy classes


package java.lang;
import java.io.*;
public class System
{
  public static PrintStream out;
}

package java.io;
public class PrintStream
{
  public void println(boolean b)  
  public void println(int i)  
  public void println(char c)  
  public void println(String s)  
  public void println()  
}

Type-checking the class Record creates a new theory Record in the same package as the class. Right-clicking this theory from the tab Symbols and selecting Print Declaration displays


theory Record uses java.lang.String, Base
{
  Record: TYPE =
    [#key: java.lang.String.String, value: Base.int,
      null: BOOLEAN, new: INT#];
  null: Record;
  newObject: INT -> Record =
    LAMBDA(x: INT): null WITH .null:=FALSE WITH .new:=x;
  Array: TYPE =
    [#value: ARRAY Base.int OF Record, length: Base.nat,
       null: BOOLEAN#];
  nullArray: Array;
  newArray: Base.nat -> Array;
  newArrayAxiom:
    AXIOM FORALL(x: Base.nat):
      LET y = newArray(x) IN
      y.null = FALSE AND y.length = x AND
      (FORALL(i: Base.nat): i < x => y.value[i] = null);
}

which introduces the following entities that mathematically model the program operations that involve program type Record.

There are some subtleties about the modeling a program object of type Record as a mathematical Record that should be known for their proper use:

  1. If the null field of a valid Record value is not FALSE, the value represents the null pointer of type Record. The Record pointer null is thus not only represented by the single mathematical constant null but by every Record value whose null field is TRUE (the constant null is just an unknown Record value for which the opposite cannot be proved)2 . A precondition that asserts that a Record object is not null must therefore state for the corresponding Record value r that r.null = FALSE holds (the condition r /= null alone is too weak).
  2. The field new is initialized to an unknown value at the creation of a record; two records created in different constructor calls can thus not be proved equal.

The program is now specified with the help of the following local theory


/*@
theory uses Base, Record, java.lang.String, java.io.PrintStream
{
  String: TYPE = java.lang.String.String;
  notFound: PREDICATE(Record.Array, Base.int, String) =
    PRED(a:Record.Array, n: Base.int, key: String):
      FORALL(i:INT):
        0 <= i AND i < n => a.value[i].key /= key;
}
@*/
class Record { … }

which introduces a predicate notFound to describe that in an array a of records, all positions less than n hold records whose keys are different from key.

The program method search can now be specified as


public static int search(Record[] a, String key) /*@
  requires
     (VAR a).null = FALSE AND (VAR key).null = FALSE AND
     (FORALL(i:INT): 0 <= i AND i < VAR a.length =>
        (VAR a).value[i].null = FALSE AND
        (VAR a).value[i].key.null = FALSE);
  ensures
    (LET result=VALUE@NEXT, n = (VAR a).length IN
      IF result = -1 THEN
        notFound(VAR a, n, VAR key)
      ELSE
        0 <= result AND result < n AND
        notFound(VAR a, result, VAR key) AND
        (VAR a).value[result].key = VAR key
      ENDIF);
@*/
{ … }

The method’s precondition states that search must not be called with the array null as argument and that its result is either -1 (indicating that the given key has not been found in the array) or that its result is the smallest index of the array such that the corresponding record has the denoted key. The specification makes use of local logical variables result and n representing the return value of the method and the length of the method parameter a.

The core loop of the method’s body can be annotated as


for (int i=0; i<n; i++)
/*@
  invariant
    (VAR a).null = FALSE AND (VAR key).null = FALSE AND
    (FORALL(i:INT): 0 <= i AND i < VAR a.length =>
       (VAR a).value[i].null = FALSE AND
       (VAR a).value[i].key.null = FALSE) AND
    VAR n = (VAR a).length AND
    0 <= VAR i AND VAR i <= VAR n AND
    notFound(VAR a, VAR i, VAR key) AND
    (RETURNS@NEXT =>
       VAR i < VAR n AND
       (VAR a).value[VAR i].key = VAR key AND
       VALUE@NEXT = VAR i);
  decreases VAR n - VAR i;
@*/
{ … }

to give a suitable invariant and termination term.

The state after type-checking the annotated program is shown  below:

Searching for Records


Figure 3.5.: Searching for Records (click to enlarge)

All type checking conditions can be automatically solved; the verification of the other conditions proceeds in a similar way as discussed in Chapter 4.

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