## 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[1] + ... + 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

download ZIP archive