This page collects hints that may help when verifying programs formally using Perfect Developer, in particular when doing the assignments for the course Formal Verification of Software.
Take a look at the examples that were installed together with Perfect Developer, in particular those regarding refinement.
Conventional testing is still a good idea before trying formal verification. Index errors, typos, or misconceptions are usually easier to detect by testing than by analysing failed proof attempts. For the small programs in the course it is probably sufficient to generate Java or C++ code with the standard settings, compile it, and run it on some test cases.
For serious testing, you should enable at least some of the debug checks (e.g. preconditions and class invariants) when generating code from PD, and use the debug version of the PD runtime library. This is especially important if you are generating code in a language such as C++ that does not itself do runtime checks e.g. that array indices are in bounds.
For more complex problems, decompose specifications and programs into smaller units by defining auxiliary functions. Identify sub-problems (like checking a particular property for the start of a sequence) and specify/refine/verify them first. Specify/refine the original problem (like checking the property for the whole sequence) by referring to the auxiliary function. Nested quantifiers and nested loops indicate situations where auxiliary functions might help.
For functions consisting essentially of a loop (which will often be the case if you decompose your problem, see above), the invariant frequently resembles the specification of the function. For finding a suitable invariant use the methods described in the lecture part of the course, in particular the replacement of constants by variables. E.g., a function and its refinement might have the following form:
function foo(A: seq of int): ...
^= ... // specification of foo
via
var x: ...
loop
var i: int != 0;
change x
keep x = foo(A.take(i)) // constant #A replaced by variable i
until (i' = #A)
decrease #A - i'
... // compute x iteratively
i! = i+1;
end;
value x
end;
Note that the invariant may refer to the specification of the
function by using its name, as in the example above. However, the use
of foo within the function is restricted to avoid
circularity problems; e.g., foo may not occur in
preconditions and assertions. You can circumvent these restrictions
by strictly separating specification from implementation:
ghost function gfoo(A: seq of int): ... ^= ... // specification of foo function foo(A: seq of int): ... ^= gfoo(A) via ... keep ... gfoo(...) ... ... assert ... gfoo(...) ... ... end;
(A ghost function does not generate code, but only defines the function in an abstract, mathematical way such that specifications and formulas like invariants and assertions can refer to it.)
If possible use similar inductive structures for invariants and loops. E.g., quantifiers, recursions, and other "loops" in the specification should iterate through arguments in the same way as the loop does. Only then Perfect Developer will be able to verify the loops without using mathematical induction. Note that PD has no induction built-in, as this would require human intervention in general (but see the next hint below). As an example, compare the following two multiplication programs. In both cases, the function is specified by recursion over the first argument. The loop of the first program iterates over the first argument:
function mult(a, b: nat): nat
decrease a
^= ([a=0]: 0, []: b+mult(a-1,b))
via
var c: nat != 0;
loop
var i: nat != 0;
change c
keep c' = mult(i',b)
until i' = a
decrease a-i';
c != c + b;
i != i + 1;
end;
value c
end;
The loop of the second program, however, iterates over the second argument:
function mult(a, b: nat): nat
decrease a
^= ([a=0]: 0, []: b+mult(a-1,b))
via
var c: nat != 0;
loop
var i: nat != 0;
change c
keep c' = mult(a,i')
until i' = b
decrease b-i';
c != a + c;
i != i + 1;
end;
value c
end;
Perfect Developer completely verifies the first program, but gives
up on two verification conditions in the second program: To show that
loop initialisation establishes the invariant, one has to prove the
inductive theorem mult(a,0)=0; similarly, to show that
the loop body preserves the invariant, one has to prove the inductive
theorem a+mult(a,b)=mult(a,b+1).
As another example, the inversions in a sequence of numbers (inversion = bigger number precedes smaller one) can be counted by iterating through the sequence and by looking either backward for elements bigger than the current one or forward for elements smaller than the current one. Using one approach for the specification and the other one for the loop requires inductive proofs, hence PD will fail to verify some properties.
If your loop uses auxiliary variables, then the invariant has to
contain information about them. Specifying just the range of the
variables is usually not sufficient. If you can verify the loop
without providing additional information, then consider replacing the
auxiliary variables and the corresponding assignments
by let-statements, since the variables apparently store
only intermediate values that are relevant just for the current
iteration.
If PD is not able to verify some verification conditions because its internal knowledge base is incomplete and lacks some crucial facts (like the inductive theorems above), then the missing pieces can be provided as axioms. If PD is able to verify the program, then the program is correct provided the axioms are valid theorems. As an example, PD is able to verify the second multiplication program above if we add the two axioms
axiom (a : nat) assert mult(a,0)=0; axiom (a,b: nat) assert a+mult(a,b)=mult(a,b+1);
As another example, PD is not able to prove that the function
function div(n,m: nat): nat pre m>0 ^= that q::0..n :- exists r::0..<m :- n=m*q+r;
specifying division of natural numbers is well defined, since it
lacks some facts from number theory allowing it to conclude that
the value q always exists and is uniquely defined. This
missing information can be either provided as axioms:
axiom (n,m: nat)
pre m>0
assert exists q::0..n :- exists r::0..<m :- n=m*q+r;
axiom (n,m: nat)
assert forall q1,q2::0..n :-
(( (exists r::0..<m :- n=m*q1+r)
&(exists r::0..<m :- n=m*q2+r)
) ==> q1=q2);
or as additional preconditions:
function div(n,m: nat): nat
pre m > 0,
(exists q::0..n :- exists r::0..<m :- n=m*q+r),
(forall q1,q2::0..n :-
(( (exists r::0..<m :- n=m*q1+r)
&(exists r::0..<m :- n=m*q2+r)
) ==> q1=q2))
^= that q::0..n :- exists r::0..<m :- n=m*q+r;
The second variant is aesthetically less pleasing but may be faster.
There is one drawback, though: Axioms increase the search space, since PD has to check their applicability thoughout the whole proof search, for all proof obligations. Hence it may happen that PD finds a proof when the axioms are not present, but exceeds some time limit when adding them.
To guide PD or to locate verification errors,
add assert statements with conditions that you think
should hold at this particular point of the program. As an example,
the four assert-statements below (obtained by applying
the rules of the Hoare calculus) are not necessary, but may help:
function mult(a, b: nat): nat
^= a*b
via
var c: nat != 0;
loop
var i: nat != 0;
change c
keep c' = i'*b
until i' = a
decrease a-i';
assert c = i*b, i ~= a;
assert c+b = (i+1)*b;
c != c + b;
assert c = (i+1)*b;
i != i + 1;
assert c = i*b;
end;
value c
end;