examples/sf.mlw

   1
   2 (* Program verification examples from the book "Software Foundations"
   3    http://www.cis.upenn.edu/~bcpierce/sf/
   4
   5    Note: we are using int (not nat), so we need extra precondition (e.g. x >= 0)
   6    Note: we are also proving termination
   7 *)
   8
   9 module HoareLogic
  10
  11   use int.Int
  12   use ref.Ref
  13
  14   (* Example: Slow Subtraction *)
  15
  16   let slow_subtraction (x: ref int) (z: ref int)
  17     requires { !x >= 0 }
  18     ensures { !z = old !z - old !x }
  19   = while !x <> 0 do
  20       invariant { 0 <= !x /\ !z - !x = old (!z - !x) } variant { !x }
  21       z := !z - 1;
  22       x := !x - 1
  23     done
  24
  25   (* Example: Reduce to Zero *)
  26
  27   let reduce_to_zero (x: ref int)
  28     requires { !x >= 0 } ensures { !x = 0 }
  29   = while !x <> 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
  30
  31   (* Exercise: Slow Addition *)
  32
  33   let slow_addition (x: ref int) (z: ref int)
  34     requires { !x >= 0 } ensures { !z = old !z + old !x }
  35   = while !x <> 0 do
  36       invariant { 0 <= !x /\ !z + !x = old (!z + !x) } variant { !x }
  37       z := !z + 1;
  38       x := !x - 1
  39     done
  40
  41   (* Example: Parity *)
  42
  43   inductive even int =
  44     | even_0 : even 0
  45     | even_odd : forall x:int. even x -> even (x+2)
  46
  47   lemma even_noneg: forall x:int. even x -> x >= 0
  48
  49   lemma even_not_odd : forall x:int. even x -> even (x+1) -> false
  50
  51   let parity (x: ref int) (y: ref int)
  52     requires { !x >= 0 } ensures { !y=0 <-> even (old !x) }
  53   = y := 0;
  54     while !x <> 0 do
  55       invariant { 0 <= !x /\ (!y=0 /\ even ((old !x) - !x) \/
  56                               !y=1 /\ even ((old !x) - !x + 1)) }
  57       variant { !x }
  58       y := 1 - !y;
  59       x := !x - 1
  60     done
  61
  62   (* Example: Finding Square Roots *)
  63
  64   let sqrt (x: ref int) (z: ref int)
  65     requires { !x >= 0 }
  66     ensures { !z * !z <= !x < (!z + 1) * (!z + 1) }
  67   = z := 0;
  68     while (!z + 1) * (!z + 1) <= !x do
  69       invariant { 0 <= !z /\ !z * !z <= !x } variant { !x - !z * !z }
  70       z := !z + 1
  71     done
  72
  73   (* Exercise: Factorial *)
  74
  75   function fact int : int
  76   axiom fact_0 : fact 0 = 1
  77   axiom fact_n : forall n:int. 0 < n -> fact n = n * fact (n-1)
  78
  79   let factorial (x: ref int) (y: ref int) (z: ref int)
  80     requires { !x >= 0 } ensures { !y = fact !x }
  81   = y := 1;
  82     z := !x;
  83     while !z <> 0 do
  84       invariant { 0 <= !z /\ !y * fact !z = fact !x } variant { !z }
  85       y := !y * !z;
  86       z := !z - 1
  87     done
  88
  89 end
  90
  91 module MoreHoareLogic
  92
  93   use int.Int
  94   use option.Option
  95   use ref.Ref
  96   use list.List
  97   use list.HdTl
  98   use list.Length
  99
 100   function sum (l : list int) : int = match l with
 101   | Nil -> 0
 102   | Cons x r -> x + sum r
 103   end
 104
 105   val head (l:list 'a) : 'a
 106     requires { l<>Nil } ensures { Some result = hd l }
 107
 108   val tail (l:list 'a) : list 'a
 109     requires { l<>Nil } ensures { Some result = tl l }
 110
 111   let list_sum (l: ref (list int)) (y: ref int)
 112     ensures { !y = sum (old !l) }
 113   = y := 0;
 114     while not (is_nil !l) do
 115       invariant { length !l <= length (old !l) /\
 116                   !y + sum !l = sum (old !l) }
 117       variant { !l }
 118       y := !y + head !l;
 119       l := tail !l
 120     done
 121
 122   use list.Mem
 123   use list.Append
 124
 125   type elt
 126   val predicate eq (x y: elt)
 127     ensures { result <-> x = y }
 128
 129   (* note: we avoid the use of an existential quantifier in the invariant *)
 130   let list_member (x : ref (list elt)) (y: elt) (z: ref int)
 131     ensures { !z=1 <-> mem y (old !x) }
 132   = z := 0;
 133     while not (is_nil !x) do
 134       invariant { length !x <= length (old !x) /\
 135                   (mem y !x -> mem y (old !x)) /\
 136                   (!z=1 /\ mem y (old !x) \/
 137                    !z=0 /\ (mem y (old !x) -> mem y !x)) }
 138       variant { !x }
 139       if eq y (head !x) then z := 1;
 140       x := tail !x
 141     done
 142
 143 end