Program verification examples from the book "Software Foundations"
Reference: Software Foundations
Authors: Jean-Christophe Filliâtre
Topics: Inductive predicates
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
(* Program verification examples from the book "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/ Note: we are using int (not nat), so we need extra precondition (e.g. x >= 0) Note: we are also proving termination *) module HoareLogic use import int.Int use import ref.Ref (* Example: Slow Subtraction *) let slow_subtraction (x: ref int) (z: ref int) = requires { !x >= 0 } ensures { !z = old !z - old !x } 'Init: while !x <> 0 do invariant { 0 <= !x /\ !z - !x = at !z 'Init - at !x 'Init } variant { !x } z := !z - 1; x := !x - 1 done (* Example: Reduce to Zero *) let reduce_to_zero (x: ref int) requires { !x >= 0 } ensures { !x = 0 } = while !x <> 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done (* Exercise: Slow Addition *) let slow_addition (x: ref int) (z: ref int) = requires { !x >= 0 } ensures { !z = old !z + old !x } 'Init: while !x <> 0 do invariant { 0 <= !x /\ !z + !x = at !z 'Init + at !x 'Init } variant { !x } z := !z + 1; x := !x - 1 done (* Example: Parity *) inductive even int = | even_0 : even 0 | even_odd : forall x:int. even x -> even (x+2) lemma even_noneg: forall x:int. even x -> x >= 0 lemma even_not_odd : forall x:int. even x -> even (x+1) -> false let parity (x: ref int) (y: ref int) requires { !x >= 0 } ensures { !y=0 <-> even (old !x) } = y := 0; 'Init: while !x <> 0 do invariant { 0 <= !x /\ (!y=0 /\ even (at !x 'Init - !x) \/ !y=1 /\ even (at !x 'Init - !x + 1)) } variant { !x } y := 1 - !y; x := !x - 1 done (* Example: Finding Square Roots *) let sqrt (x: ref int) (z: ref int) requires { !x >= 0 } ensures { !z * !z <= !x < (!z + 1) * (!z + 1) } = z := 0; while (!z + 1) * (!z + 1) <= !x do invariant { 0 <= !z /\ !z * !z <= !x } variant { !x - !z * !z } z := !z + 1 done (* Exercise: Factorial *) function fact int : int axiom fact_0 : fact 0 = 1 axiom fact_n : forall n:int. 0 < n -> fact n = n * fact (n-1) let factorial (x: ref int) (y: ref int) (z: ref int) requires { !x >= 0 } ensures { !y = fact !x } = y := 1; z := !x; while !z <> 0 do invariant { 0 <= !z /\ !y * fact !z = fact !x } variant { !z } y := !y * !z; z := !z - 1 done end module MoreHoareLogic use import int.Int use import option.Option use import ref.Ref use import list.List use import list.HdTl use import list.Length function sum (l : list int) : int = match l with | Nil -> 0 | Cons x r -> x + sum r end val head (l:list 'a) : 'a requires { l<>Nil } ensures { Some result = hd l } val tail (l:list 'a) : list 'a requires { l<>Nil } ensures { Some result = tl l } let list_sum (l: ref (list int)) (y: ref int) ensures { !y = sum (old !l) } = y := 0; 'Init: while !l <> Nil do invariant { length !l <= length (at !l 'Init) /\ !y + sum !l = sum (at !l 'Init) } variant { !l } y := !y + head !l; l := tail !l done use import list.Mem use import list.Append (* note: we avoid the use of an existential quantifier in the invariant *) let list_member (x : ref (list 'a)) (y: 'a) (z: ref int) ensures { !z=1 <-> mem y (old !x) } = z := 0; 'Init: while !x <> Nil do invariant { length !x <= length (at !x 'Init) /\ (mem y !x -> mem y (at !x 'Init)) /\ (!z=1 /\ mem y (at !x 'Init) \/ !z=0 /\ (mem y (at !x 'Init) -> mem y !x)) } variant { !x } if y = head !x then z := 1; x := tail !x done end
download ZIP archive