examples/find.mlw

   1
   2 (*
   3  C. A. R. Hoare.
   4  Proof of a program: Find.
   5  Commun. ACM, 14:39--45, January 1971.
   6 *)
   7
   8 module FIND
   9
  10   use int.Int
  11   use ref.Ref
  12   use array.Array
  13   use array.ArrayPermut
  14
  15   val constant _N: int (* actually N in Hoare's notation *)
  16   val constant f: int
  17
  18   axiom f_N_range: 1 <= f <= _N
  19
  20   predicate found (a: array int) =
  21     forall p q:int. 1 <= p <= f <= q <= _N -> a[p] <= a[f] <= a[q]
  22
  23   predicate m_invariant (m: int) (a: array int) =
  24     m <= f /\ forall p q:int. 1 <= p < m <= q <= _N -> a[p] <= a[q]
  25
  26   predicate n_invariant (n: int) (a: array int) =
  27     f <= n /\ forall p q:int. 1 <= p <= n < q <= _N -> a[p] <= a[q]
  28
  29   predicate i_invariant (m n i q r: int) (a: array int) =
  30     m <= i /\ (forall p:int. 1 <= p < i -> a[p] <= r) /\
  31     (i <= n -> i <= q <= n /\ r <= a[q])
  32
  33   predicate j_invariant (m n j p r: int) (a: array int) =
  34     j <= n /\ (forall q:int. j < q <= _N -> r <= a[q]) /\
  35     (m <= j -> m <= p <= j /\ a[p] <= r)
  36
  37   predicate termination (i j i0 j0 r: int) (a:array int) =
  38     (i > i0 /\ j < j0) \/ (i <= f <= j /\ a[f] = r)
  39
  40   let find (a: array int) =
  41     requires { length a = _N+1 }
  42     ensures  { found a /\ permut_all a (old a) }
  43   let m = ref 1 in let n = ref _N in
  44   while !m < !n do
  45     invariant { m_invariant !m a /\ n_invariant !n a /\
  46       permut_all a (old a) /\ 1 <= !m /\ !n <= _N }
  47     variant { !n - !m }
  48     let r = a[f] in let i = ref !m in let j = ref !n in
  49     let ghost p = ref f in let ghost q = ref f in
  50     while !i <= !j do
  51       invariant { i_invariant !m !n !i !q r a /\ j_invariant !m !n !j !p r a /\
  52         m_invariant !m a /\ n_invariant !n a /\ 0 <= !j /\ !i <= _N + 1 /\
  53         termination !i !j !m !n r a /\ permut_all a (old a) }
  54       variant { _N + 2 + !j - !i }
  55       label L in
  56       while a[!i] < r do
  57         invariant { i_invariant !m !n !i !q r a /\
  58           !i at L <= !i <= !n /\ termination !i !j !m !n r a }
  59         variant { _N + 1 - !i }
  60         i := !i + 1
  61       done;
  62
  63       while r < a[!j] do
  64         invariant { j_invariant !m !n !j !p r a /\
  65           !j <= !j at L /\ !m <= !j /\ termination !i !j !m !n r a }
  66         variant { !j }
  67         j := !j - 1
  68       done;
  69
  70       assert { a[!j] <= r <= a[!i] };
  71
  72       if !i <= !j then begin
  73         let w = a[!i] in begin a[!i] <- a[!j]; a[!j] <- w end;
  74         assert { exchange a (a at L) !i !j };
  75         ghost begin
  76           p := if !i < !j then !i else !j - 1;
  77           q := if !i < !j then !j else !i + 1
  78         end;
  79         i := !i + 1;
  80         j := !j - 1
  81       end
  82     done;
  83
  84     assert { !m < !i /\ !j < !n };
  85
  86     if f <= !j then
  87       n := !j
  88     else if !i <= f then
  89       m := !i
  90     else
  91       begin n := f; m := f end
  92   done
  93
  94 end