new example: FIND

parent b6a697b5
(*
C. A. R. Hoare.
Proof of a program: Find.
Commun. ACM, 14:39--45, January 1971.
*)
module FIND
use import int.Int
use import module ref.Ref
use import module array.Array
use import module array.ArrayPermut
function _N: int (* actually N in Hoare's notation *)
function f: int
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) =
{ length a = _N+1 }
'Init:
let m = ref 1 in let n = ref _N in
while !m < !n do
invariant { m_invariant !m a /\ n_invariant !n a /\ permut a (at a 'Init)
/\ 1 <= !m /\ !n <= _N }
variant { !n - !m }
let r = a[f] in let i = ref !m in let j = ref !n in
while !i <= !j do
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
/\ termination !i !j !m !n r a
/\ permut a (at a 'Init) }
variant { _N + 2 + !j - !i }
'L: while a[!i] < r do
invariant { i_invariant !m !n !i r a
/\ at !i 'L <= !i <= !n
/\ termination !i !j !m !n r a }
variant { _N + 1 - !i }
i := !i + 1
done;
while r < a[!j] do
invariant { j_invariant !m !n !j r a
/\ !j <= at !j 'L /\ !m <= !j
/\ termination !i !j !m !n r a }
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
{ found a /\ permut a (old a) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/find.gui"
End:
*)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| mk_array _ elts1 => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| mk_array length1 _ => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
(u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
Implicit Arguments map_eq_sub.
Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z)
(j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))).
Implicit Arguments exchange.
Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z)
(j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j).
Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
| permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
(u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
(j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
Implicit Arguments permut_sub.
Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z
a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\
(r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z),
((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))).
Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2
i) = (get a1 j)).
Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z)
(j:Z): Prop := (exchange (elts a1) (elts a2) i j).
Implicit Arguments exchange1.
Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
Implicit Arguments permut_sub1.
Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z
(length a1)).
Implicit Arguments permut.
Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a))
(i:Z) (j:Z), (exchange1 a1 a2 i j) -> (((length a1) = (length a2)) ->
(((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\
(j < (length a1))%Z) -> (permut a1 a2)))).
Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
Implicit Arguments array_eq_sub.
Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)).
Implicit Arguments array_eq.
Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u).
Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)), (array_eq a1 a2) -> (permut a1 a2).
Parameter usN: Z.
Parameter f: Z.
Axiom f_N_range : (1%Z <= (f ))%Z /\ ((f ) <= (usN ))%Z.
Definition found(a:(array Z)): Prop := forall (p:Z) (q:Z), ((((1%Z <= p)%Z /\
(p <= (f ))%Z) /\ ((f ) <= q)%Z) /\ (q <= (usN ))%Z) -> (((get1 a
p) <= (get1 a (f )))%Z /\ ((get1 a (f )) <= (get1 a q))%Z).
Definition m_invariant(m:Z) (a:(array Z)): Prop := (m <= (f ))%Z /\
forall (p:Z) (q:Z), ((((1%Z <= p)%Z /\ (p < m)%Z) /\ (m <= q)%Z) /\
(q <= (usN ))%Z) -> ((get1 a p) <= (get1 a q))%Z.
Definition n_invariant(n:Z) (a:(array Z)): Prop := ((f ) <= n)%Z /\
forall (p:Z) (q:Z), ((((1%Z <= p)%Z /\ (p <= n)%Z) /\ (n < q)%Z) /\
(q <= (usN ))%Z) -> ((get1 a p) <= (get1 a q))%Z.
Definition i_invariant(m:Z) (n:Z) (i:Z) (r:Z) (a:(array Z)): Prop :=
(m <= i)%Z /\ ((forall (p:Z), ((1%Z <= p)%Z /\ (p < i)%Z) -> ((get1 a
p) <= r)%Z) /\ ((i <= n)%Z -> exists p:Z, ((i <= p)%Z /\ (p <= n)%Z) /\
(r <= (get1 a p))%Z)).
Definition j_invariant(m:Z) (n:Z) (j:Z) (r:Z) (a:(array Z)): Prop :=
(j <= n)%Z /\ ((forall (q:Z), ((j < q)%Z /\ (q <= (usN ))%Z) ->
(r <= (get1 a q))%Z) /\ ((m <= j)%Z -> exists q:Z, ((m <= q)%Z /\
(q <= j)%Z) /\ ((get1 a q) <= r)%Z)).
Definition termination(i:Z) (j:Z) (i0:Z) (j0:Z) (r:Z) (a:(array Z)): Prop :=
((i0 < i)%Z /\ (j < j0)%Z) \/ (((i <= (f ))%Z /\ ((f ) <= j)%Z) /\
((get1 a (f )) = r)).
Theorem WP_parameter_find : forall (a:Z), forall (a1:(map Z Z)), let a2 :=
(mk_array a a1) in ((a = ((usN ) + 1%Z)%Z) -> forall (n:Z), forall (m:Z),
forall (a3:(map Z Z)), let a4 := (mk_array a a3) in (((m_invariant m a4) /\
((n_invariant n a4) /\ ((permut a4 a2) /\ ((1%Z <= m)%Z /\
(n <= (usN ))%Z)))) -> ((m < n)%Z -> (((0%Z <= (f ))%Z /\
((f ) < a)%Z) -> let result := (get a3 (f )) in forall (j:Z),
forall (i:Z), forall (a5:(map Z Z)), let a6 := (mk_array a a5) in
(((i_invariant m n i result a6) /\ ((j_invariant m n j result a6) /\
((m_invariant m a6) /\ ((n_invariant n a6) /\ ((0%Z <= j)%Z /\
((i <= ((usN ) + 1%Z)%Z)%Z /\ ((termination i j m n result a6) /\
(permut a6 a2)))))))) -> ((i <= j)%Z -> forall (i1:Z), ((i_invariant m n i1
result a6) /\ (((i <= i1)%Z /\ (i1 <= n)%Z) /\ (termination i1 j m n result
a6))) -> (((0%Z <= i1)%Z /\ (i1 < a)%Z) -> ((~ ((get a5
i1) < result)%Z) -> forall (j1:Z), ((j_invariant m n j1 result a6) /\
((j1 <= j)%Z /\ ((m <= j1)%Z /\ (termination i1 j1 m n result a6)))) ->
(((0%Z <= j1)%Z /\ (j1 < a)%Z) -> ((~ (result < (get a5 j1))%Z) ->
((((get a5 j1) <= result)%Z /\ (result <= (get a5 i1))%Z) ->
((i1 <= j1)%Z -> (((0%Z <= i1)%Z /\ (i1 < a)%Z) -> (((0%Z <= j1)%Z /\
(j1 < a)%Z) -> (((0%Z <= i1)%Z /\ (i1 < a)%Z) -> forall (a7:(map Z Z)),
(a7 = (set a5 i1 (get a5 j1))) -> (((0%Z <= j1)%Z /\ (j1 < a)%Z) ->
forall (a8:(map Z Z)), (a8 = (set a7 j1 (get a5 i1))) -> ((exchange a8 a5
i1 j1) -> (((get a8 i1) <= result)%Z -> ((result <= (get a8 j1))%Z ->
forall (i2:Z), (i2 = (i1 + 1%Z)%Z) -> forall (j2:Z), (j2 = (j1 - 1%Z)%Z) ->
(permut (mk_array a a8) a2)))))))))))))))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
unfold permut; simpl.
intuition.
apply permut_trans with a5.
apply permut_exchange with i1 j1; intuition.
red in H17.
simpl in H17.
intuition.
Qed.
(* DO NOT EDIT BELOW *)
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment