Program Verification

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.