## 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 int.Int
use ref.Ref

(* Example: Slow Subtraction *)

let slow_subtraction (x: ref int) (z: ref int)
requires { !x >= 0 }
ensures { !z = old !z - old !x }
= while !x <> 0 do
invariant { 0 <= !x /\ !z - !x = old (!z - !x) } 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

let slow_addition (x: ref int) (z: ref int)
requires { !x >= 0 } ensures { !z = old !z + old !x }
= while !x <> 0 do
invariant { 0 <= !x /\ !z + !x = old (!z + !x) } 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;
while !x <> 0 do
invariant { 0 <= !x /\ (!y=0 /\ even ((old !x) - !x) \/
!y=1 /\ even ((old !x) - !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 int.Int
use option.Option
use ref.Ref
use list.List
use list.HdTl
use 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;
while not (is_nil !l) do
invariant { length !l <= length (old !l) /\
!y + sum !l = sum (old !l) }
variant { !l }
y := !y + head !l;
l := tail !l
done

use list.Mem
use list.Append

type elt
val predicate eq (x y: elt)
ensures { result <-> x = y }

(* note: we avoid the use of an existential quantifier in the invariant *)
let list_member (x : ref (list elt)) (y: elt) (z: ref int)
ensures { !z=1 <-> mem y (old !x) }
= z := 0;
while not (is_nil !x) do
invariant { length !x <= length (old !x) /\
(mem y !x -> mem y (old !x)) /\
(!z=1 /\ mem y (old !x) \/
!z=0 /\ (mem y (old !x) -> mem y !x)) }
variant { !x }
if eq y (head !x) then z := 1;
x := tail !x
done

end
```