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