Program Verification
- From logic specification to verified (WhyML) implementation(s)
- Verifying why3k assembly to its logic specification.
From logic specification to verified (WhyML) implementation(s)
Let us assume the
sum function (see below). The
sum_rec is a recursive implementation, while
sum_loop is an imperative version. The
variant keyword is used to indicate that
i will decrease, and thus ensure termination (when $i=0$, the
else branch is taken and the function returns
0).
ref denotes a
reference, and
! is used to
de-referencing.
module Sum
use import int.Int
use import ref.Ref
(*
Informal specification:
take an integer argument i
compute the sum of numbers 0+1+2..+i
*)
let rec sum_rec ( i : int ) : int
variant { i }
= if (i > 0) then i + sum_rec (i - 1) else 0
let sum_loop ( i : int ) : int
= let r = ref 0 in
for j = 1 to i do
r := !r + i;
done;
!r
end
You may ask, are these implementations correct with respect to our informal specification, and are these replaceable? (I.e., can we safely chose either one depending on some non-functional property, e.g., memory consumption or execution efficiency?)
To that end we need a specification!
(* this is NOT a function it is an inductive predicate *)
inductive sum (int) (int) =
| Sum_0 : forall i r:int. i <= 0 /\ r = 0 -> sum i r
| Sum_n : forall i r:int. i > 0 -> sum (i-1) r -> sum i (i + r)
The
sum inductive predicate defines the set of (integer) points
i (input)
r (output) which
sum i r holds.
Sum_0 gives the points
sum 0 0", sum (-1) 0", ...
sum (- inf) 0, i.e. for which the result
r is
0. And
Sum_n the
inductive case, starting from
sum 0 0,
i - 1 = 0, "r=0". It implies
sum i (i r), i.e.,
sum 1 (10) .
sum 1 1 -> sum 2 (210) which implies
sum 3 (3 2 1 + 0), and there you go....to infinitely. This specification, makes sense in comparison to our informal understanding of the problem at hand, right?
Now we can relate the implementation to the specification. The
ensures assert the predicate
sum i result, i.e., for any
i (parameter)
sum i result should hold (
result being the return value of the function). Notice, the implementation follows the
sum predicate
then branch is a direct match to the
Sum_n, while the
else branch is a direct match to
Sum_0. The
why3 platform should be able to
discharge the (
ensures) assertion and pass the implementation as being correct w.r.t the specification.
let rec sum_rec' ( i : int ) : int
variant { i }
ensures { sum i result }
= if (i > 0) then i + sum_rec' (i - 1) else 0
We may now turn to the imperative
sum_loop. here we explicitly have to assert the
base case (
assert { sum 0 !r};) and the inductive case
invariant { sum (j-1) !r }. The
why3 platform should be able to
discharge the (
ensures) assertion and pass the implementation as being correct w.r.t the specification. Notice,
j is the index in the loop, hence for first iteration
j-1=0, which asserts
sum 0 0 which is also holds according to specification.
let sum_loop' ( i : int ) : int
ensures { sum i result }
= let r = ref 0 in
assert { sum 0 !r};
for j = 1 to i do
invariant { sum (j-1) !r }
r := !r + j;
done;
!r
Finally in preparation for verifying the
why3k assembly version, we replace the
whyML references to
j in the for loop, by a local (mutable) variable
t1, and use the
v0 variable to hold our result. Notice,
j is now only used for the
verification and
iteration.
let sum_loop_asm' ( i : int ) : int
ensures { sum i result }
= let v0 = ref 0 in
let t1 = ref 1 in
assert { sum 0 !v0};
for j = 1 to i do
invariant { sum (!t1-1) !v0 }
invariant { !t1 = j }
v0 := !v0 + !t1;
t1 := !t1 + 1;
done;
!v0
We can now manually assert the set of implementations presented. As expected, without the
contract why3 is not able to prove the result (and with the contract is does)! We now have gone from informal specification and mere implementations, to formal specified functions with proven implementations. Good job everyone!
let test()
=
let r = sum_rec 3 in
assert { r = 6 }; (* will fail, lacking contract *)
let r = sum_loop 3 in
assert { r = 6 }; (* will fail, lacking contract *)
let r = sum_loop' 3 in
assert { r = 6 };
let r = sum_rec' 3 in
assert { r = 6 };
let r = sum_loop_asm' 3 in
assert { r = 6 };
()
end
Verifying why3k assembly to its logic specification.
/Per Lindgren, September 2015.