why3/examples/sf.mlw

(* 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

  (* Exercise: Slow Addition *)

  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