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.