procedure_prove

procedure_prove is a termination and/or safety prover for simple procedural imperative programs. It shares its program syntax with the while_prove prover, but also supports procedures, which may be recursive, that have a pass-by-value semantics for parameters. Procedure specifications in the form of pre-/postcondition pairs must be given, where pre- and postconditions are given by SL formulas.

The prover comes with a benchmark suite of around 40 test programs. This comprises around 20 custom benchmarks, as well as around 20 examples taken from the Java_bytecode_recursive section of the Termination Problems Database.

Compiling & Running

After downloading the source code from Github, follow the installation instructions and compile by running make. This will produce an executable called procedure_prove.native.

Running procedure_prove.native without options will produce some help text explaining its usage. You can specify on the command line which procedures you wish to be analysed. If no procedures are given on the command line, the tool will look for a main procedure. You can specify that all procedures in the input file should be analysed by giving the command-line option -all. By default, the prover will analyse an input program for memory safe execution only; if you wish the prover to also prove termination of the program, run the executable with the command-line option -T.

Example

The following program (included in the benchmark suite as 23-cls-rec.wl2) traverses a cyclic linked list.

fields: next;

proc traverselist(x, end)
  precondition: ls(x, end);
  postcondition: ls(x, end);
{
  if x != end then
  
    y := x.next;
    traverselist(y, end)
  
  fi
}

proc main(x)
  precondition: cls(x);
  postcondition: cls(x);
{
  y := x.next;
  traverselist(y, x)
}

The first line declares that heap cells are records with one field, called next (this program is for use with linked lists).

The program consists of two procedures, traverselist and main, each with a pre-/postcondition specification. The specification of traverselist asserts that the precondition for (safely) calling the procedure is that the memory is described by the inductive predicate ls, whose definition is as follows (see sl_prove for details on how to interpret the definition):

ls { 
	x=y => ls(x,y) | 
	x!=y * x->x' * ls(x',y) => ls(x,y) 
}

That is, the memory must contain a linked list segment whose head is referenced by its first parameter x, and whose last element is referenced by the second parameter end. The specification of the main procedure is that its parameter x must reference a cyclic linked list, which is expressed by the predicate cls whose definition is as follows:

cls {
	x->y' * ls(y',x) => cls(x) 
}

Let’s verify that this program terminates safely (i.e., without committing memory faults).

$ ./procedure_prove.native -T -P benchmarks/procs/23-cls-rec.wl2 -p
0:  |- {ls[a](x, end)} traverselist(x, end) {ls[a'](x, end)} (Proc Unf. traverselist) [1 <{(a, a)}/{}>]
  1:  |- {ls[a](x, end)} 0: if x!=end then 1: ... fi {ls[a'](x, end)} (If) [2 <{(a, a)}/{}>, 3 <{(a, a)}/{}>]
    2:  |- {x!=end * ls[a](x, end)} 1: y := x.next; 2: ... {ls[a'](x, end)} (ls L.Unf.) [4 <{(a, a)}/{(a, b')}>, 5 <{(a, a)}/{(a, b')}>]
      4:  |- {[b' < a] : x=end * x!=end} 1: y := x.next; 2: ... {ls[a'](x, end)} (Ex Falso)
      5:  |- {[b' < a] : nil!=x * x!=end * x->w' * ls[b'](w', end)} 1: y := x.next; 2: ... {ls[a'](x, end)} (Load/Simplify) [6 <{(b', b'), (a, a)}/{}>]
        6:  |- {[b' < a] : nil!=x * x!=end * x->y * ls[b'](y, end)} 2: traverselist(y, end) {ls[a'](x, end)} (Ex.Intro.) [7 <{(b', b), (a, a)}/{}>]
          7:  |- {[b < a] : nil!=x * x!=end * x->y * ls[b](y, end)} 2: traverselist(y, end) {ls[a'](x, end)} (RHS.Conseq) [8 <{(b, b), (a, a)}/{}>]
            8:  |- {[b < a] : nil!=x * x!=end * x->y * ls[b](y, end)} traverselist(y, end) {[b < a] : nil!=x * x!=end * x->y * ls[a'](y, end)} (Frame) [9 <{(b, b)}/{}>]
              9:  |- {ls[b](y, end)} traverselist(y, end) {ls[a'](y, end)} (Subst) [10 <{(b, a)}/{}>]
                10:  |- {ls[a](y, end)} traverselist(y, end) {ls[a'](y, end)} (Param Subst) [11 <{(a, a)}/{}>]
                  11:  |- {ls[a](x, end)} traverselist(x, end) {ls[a'](x, end)} (Backl) [0] <pre={(a, a)}>
    3:  |- {x=end * ls[a](x, end)}  {ls[a'](x, end)} (Axiom)

0:  |- {cls[a](x)} main(x) {cls[a'](x)} (Proc Unf. main) [1 <{(a, a)}/{}>]
  1:  |- {cls[a](x)} 0: y := x.next; 1: ... {cls[a'](x)} (cls L.Unf.) [2 <{(a, a)}/{(a, b')}>]
    2:  |- {[b' < a] : nil!=x * x->w' * ls[b'](w', x)} 0: y := x.next; 1: ... {cls[a'](x)} (Load/Simplify) [3 <{(b', b'), (a, a)}/{}>]
      3:  |- {[b' < a] : nil!=x * x->y * ls[b'](y, x)} 1: traverselist(y, x) {cls[a'](x)} (Ex.Intro.) [4 <{(b', b), (a, a)}/{}>]
        4:  |- {[b < a] : nil!=x * x->y * ls[b](y, x)} 1: traverselist(y, x) {cls[a'](x)} (RHS.Conseq) [5 <{(b, b), (a, a)}/{}>]
          5:  |- {[b < a] : nil!=x * x->y * ls[b](y, x)} traverselist(y, x) {[b < a] : nil!=x * x->y * ls[a'](y, x)} (Frame) [6 <{(b, b)}/{}>]
            6:  |- {ls[b](y, x)} traverselist(y, x) {ls[a'](y, x)} (Subst) [7 <{(b, a)}/{}>]
              7:  |- {ls[a](y, x)} traverselist(y, x) {ls[a'](y, x)} (Param Subst) [8 <{(a, a)}/{}>]
                8:  |- {ls[a](x, end)} traverselist(x, end) {ls[a'](x, end)} (Proc Unf. traverselist) [9 <{(a, a)}/{}>]
                ...

The output shows (textual representations of) cyclic termination proofs for the two procedures. Notice that the traverselist procedure is analysed before main since main depends on (i.e. makes a call to) traverselist. Thus, the proof of main actually includes the proof of traverselist as a sub-proof, however we elide this in the output above. The recursion in the traverselist procedure is handled in the cyclic proof by a back-link, which can be seen in node 11 of the proof above.

Each predicate is marked with a variable, e.g. ls[a](x, end). At points in the proof where the analysis splits on each case of the predicate definition (e.g. at node 2 in the first proof above), newly introduced predicates are given fresh variables and constraints are introduced between these fresh variables and that of the unfolded predicate, e.g. [b' < a]. Cyclist uses these variables to construct termination measures for programs, and the constraints indicate when these measures decrease. The proof above indicates how the measures track from one node to the next. For example, in the first proof above, node 2 has two successors: nodes 4 and 5. We can track the measure from variable a in node 2 to variables a and b' in each of its successors. Moreover, when we track the measure from a to b' the termination measure decreases.

In this example, the termination measure tracked by Cyclist coincides with the length of the linked list: each (recursive) call to the traverselist procedure moves one link along the linked list. Cyclist verifies termination by ensuring that some termination measure decreases in every cycle in the proof.

Benchmarks

To run the benchmarks test do

$ make proc-tests

To obtain more information from the tests, the shell variable TST_OPTS will add command-line arguments to procedure_prove. For example, the command

TST_OPTS=-s make proc-tests

will produce statistics for each test, including runtimes.