## Program proofs from Floyd's Assigning Meanings to Programs (1967)

Authors: Jean-Christophe Filliâtre

Topics: Historical examples

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```(* Program proofs from Floyd's "Assigning Meanings to Programs" (1967) *)

module Sum

(* computes the sum a + ... + a[n] *)

use int.Int
use ref.Ref
use array.Array
use array.ArraySum

let sum (a: array int) (n: int)
requires { 0 <= n < a.length }
ensures  { result = sum a 1 (n+1) }
= let i = ref 1 in
let s = ref 0 in
while !i <= n do
invariant { 1 <= !i <= n+1 /\ !s = sum a 1 !i }
variant { n - !i }
s := !s + a[!i];
i := !i + 1
done;
!s

end

module Division

(* Quotient and remainder of X div Y

Floyd's lexicographic variant is unnecessarily complex here, since
we do not seek for a variant which decreases at each statement, but
only at each execution of the loop body. *)

use int.Int
use ref.Ref

let division (x: int) (y: int) : (q: int, r: int)
requires { 0 <= x /\ 0 < y }
ensures  { 0 <= r < y /\ x = q * y + r }
= let q = ref 0 in
let r = ref x in
while !r >= y do
invariant { 0 <= !r /\ x = !q * y + !r }
variant { !r }
r := !r - y;
q := !q + 1
done;
!q, !r

end
```