while_prove
while_prove
is a termination and/or safety prover for simple while-programs
specified by preconditions in SL. Postconditions are not used, so the prover does not
check for memory leaks or producing a specific heap after execution.
The while_prove
tool is a significantly changed and updated version of the
goto_prove
tool presented in the [APLAS12]. The goto_prove
tool is deprecated
and unmaintained; if you are interested in seeing the source code or running it see below.
Compiling
If you are simply looking for the latest version of while_prove
, have a look at Installation.
The original version of goto_prove
in [APLAS12] is not stored on GitHub. To try the closest possible,
you can checkout a very early commit.
git clone https://github.com/ngorogiannis/cyclist.git cyclist
cd cyclist
git checkout b289f39a6a46b4f57da3585aa7fd71f3ca8601fc
Then consult the README included, which contains building instructions relevant to that version.
Running while_prove.native
without options will produce some help text explaining its usage.
Example
Here is a program for use with while_prove
.
fields: next;
precondition: ls(x,nil);
while x!=nil do
x := x.next
od
The first line declares that heap cells are records with one field, called next
(this program is for use with linked lists).
The second line states the precondition of the program.
The remainder is code in a while-language with if/while control structures and assignment/dereference.
Let’s verify that this program terminates safely (i.e., without committing memory faults).
$ ./while_prove.native -T -P benchmarks/whl/01-ls.wl -p
0: ls^1(x, nil) |- 0: while x!=nil do 1: ... od (While) [1, 2]
1: nil!=x * ls^1(x, nil) |- 1: x := x.next; 0: ... (ls L.Unf.) [3, 4]
3: nil=x * nil!=x |- 1: x := x.next; 0: ... (Ex Falso)
4: nil!=x * x->y' * ls^1(y', nil) |- 1: x := x.next; 0: ... (Load/Simplify) [5]
5: nil!=x' * x'->x * ls^1(x, nil) |- 0: while x!=nil do 1: ... od (Frame) [6]
6: ls^1(x, nil) |- 0: while x!=nil do 1: ... od (Backl) [0] <pre={(1, 1)}>
2: nil=x * ls^1(x, nil) |- (Empty)
The output includes a cyclic proof of termination (effectively an argument that the linked list provided as input is consumed as the program runs).
Benchmarks in [APLAS12]
The benchmarks in [APLAS12] were for the goto_prove
tool which is no longer maintained.
Translated versions of these benchmarks are included in the Cyclist repository under
benchmarks/whl
.
To run these benchmarks do
$ make whl-tests
To obtain more information from the tests, the shell variable
TST_OPTS
will add command-line arguments to while_prove
.
For example, the command
TST_OPTS=-s make whl-tests
will produce statistics for each test, including runtimes.