 ### insertion sort examples: added generic versions

parent bb609f33
 ... ... @@ -35,3 +35,51 @@ module InsertionSort done end module InsertionSortGen use import int.Int use import ref.Ref use import array.Array use import array.ArrayPermut use import array.ArrayEq clone import map.MapSorted as M axiom le_refl: forall x:elt. le x x axiom le_asym: forall x y:elt. not (le x y) -> le y x axiom le_trans: forall x y z:elt. le x y /\ le y z -> le x z predicate sorted_sub (a : array elt) (l u : int) = M.sorted_sub a.elts l u predicate sorted (a : array elt) = M.sorted_sub a.elts 0 a.length let insertion_sort (a: array elt) = ensures { sorted a /\ permut (old a) a } 'L: for i = 1 to length a - 1 do (* a[0..i[ is sorted; now insert a[i] *) invariant { sorted_sub a 0 i /\ permut (at a 'L) a } let v = a[i] in let j = ref i in while !j > 0 && not (le a[!j - 1] v) do invariant { 0 <= !j <= i } invariant { permut (at a 'L) a[!j <- v] } invariant { forall k1 k2: int. 0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> le a[k1] a[k2] } invariant { forall k: int. !j+1 <= k <= i -> le v a[k] } variant { !j } 'L1: a[!j] <- a[!j - 1]; assert { exchange (at a 'L1)[!j <- v] a[!j-1 <- v] (!j - 1) !j }; j := !j - 1 done; assert { forall k: int. 0 <= k < !j -> le a[k] v }; a[!j] <- v done end
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive ref (a:Type) {a_WT:WhyType a} := | mk_ref : a -> ref a. Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a). Existing Instance ref_WhyType. Implicit Arguments mk_ref [[a] [a_WT]]. (* Why3 assumption *) Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a := match v with | (mk_ref x) => x end. Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b). Existing Instance map_WhyType. Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b. Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b -> (map a b). Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, 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} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, 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 {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, b -> (map a b). Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). (* Why3 assumption *) Inductive array (a:Type) {a_WT:WhyType a} := | mk_array : Z -> (map Z a) -> array a. Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a). Existing Instance array_WhyType. Implicit Arguments mk_array [[a] [a_WT]]. (* Why3 assumption *) Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) := match v with | (mk_array x x1) => x1 end. (* Why3 assumption *) Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z := match v with | (mk_array x x1) => x end. (* Why3 assumption *) Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := (get (elts a1) i). (* Why3 assumption *) Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array a) := (mk_array (length a1) (set (elts a1) i v)). (* Why3 assumption *) Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) := (mk_array n (const v:(map Z a))). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a}(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)). (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a}(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))). Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, 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). (* Why3 assumption *) Inductive permut_sub{a:Type} {a_WT:WhyType a} : (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))). Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, 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} {a_WT:WhyType a}, forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (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} {a_WT:WhyType a}, 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)). (* Why3 assumption *) Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a)) (i:Z) (j:Z): Prop := (exchange (elts a1) (elts a2) i j). (* Why3 assumption *) Definition permut_sub1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a)) (l:Z) (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a)): Prop := ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z (length a1)). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, 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)))). Axiom permut_sym1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)), (permut a1 a2) -> (permut a2 a1). Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). (* Why3 assumption *) Definition array_eq_sub {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). (* Why3 assumption *) Definition array_eq {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a)): Prop := ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)). Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a}, 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} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2). Axiom elt : Type. Parameter elt_WhyType : WhyType elt. Existing Instance elt_WhyType. Parameter le: elt -> elt -> Prop. (* Why3 assumption *) Definition sorted_sub(a:(map Z elt)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> (le (get a i1) (get a i2)). Axiom le_refl : forall (x:elt), (le x x). Axiom le_asym : forall (x:elt) (y:elt), (~ (le x y)) -> (le y x). Axiom le_trans : forall (x:elt) (y:elt) (z:elt), ((le x y) /\ (le y z)) -> (le x z). (* Why3 assumption *) Definition sorted_sub1(a:(array elt)) (l:Z) (u:Z): Prop := (sorted_sub (elts a) l u). (* Why3 assumption *) Definition sorted(a:(array elt)): Prop := (sorted_sub (elts a) 0%Z (length a)). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z elt)), let a2 := (mk_array a a1) in ((1%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z elt)), forall (i:Z), ((1%Z <= i)%Z /\ (i <= (a - 1%Z)%Z)%Z) -> (((sorted_sub a3 0%Z i) /\ (permut a2 (mk_array a a3))) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let v := (get a3 i) in forall (j:Z) (a4:(map Z elt)), (((((0%Z <= j)%Z /\ (j <= i)%Z) /\ (permut a2 (mk_array a (set a4 j v)))) /\ forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) -> ((~ (k1 = j)) -> ((~ (k2 = j)) -> (le (get a4 k1) (get a4 k2))))) /\ forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (le v (get a4 k))) -> ((0%Z < j)%Z -> (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < a)%Z) -> ((~ (le (get a4 (j - 1%Z)%Z) v)) -> (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < a)%Z) -> (((0%Z <= j)%Z /\ (j < a)%Z) -> forall (a5:(map Z elt)), (a5 = (set a4 j (get a4 (j - 1%Z)%Z))) -> ((exchange (set a4 j v) (set a5 (j - 1%Z)%Z v) (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2 (mk_array a (set a5 j1 v)))))))))))). intros a a1 a2 h1 a3 i (h2,h3) (h4,h5) (h6,h7) v j a4 ((((h8,h9),h10),h11),h12) h13 (h14,h15) h16 (h17,h18) (h19,h20) a5 h21 h22 j1 h23. unfold permut in *. simpl; split; auto. simpl in h10. destruct h10 as (h10a & h10b). apply permut_trans with (1:=h10b). ae. Qed.
This diff is collapsed.
 ... ... @@ -42,4 +42,56 @@ module InsertionSortDumb done end \ No newline at end of file end module InsertionSortDumbGen use import int.Int use import ref.Ref use import ref.Refint use import array.Array use import array.ArrayPermut clone import map.MapSorted as M axiom le_refl: forall x:elt. le x x axiom le_asym: forall x y:elt. not (le x y) -> le y x axiom le_trans: forall x y z:elt. le x y /\ le y z -> le x z predicate sorted_sub (a : array elt) (l u : int) = M.sorted_sub a.elts l u predicate sorted (a : array elt) = M.sorted_sub a.elts 0 a.length let sort (a:array elt) ensures { sorted a } ensures { permut (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut (at a 'Init) a } invariant { sorted_sub a 0 i } let j = ref i in while !j > 0 && not (le a[!j-1] a[!j]) do invariant { 0 <= !j <= i } invariant { permut (at a 'Init) a } invariant { sorted_sub a 0 !j } invariant { sorted_sub a !j (i+1) } invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i -> le a[k1] a[k2] } 'L: let b = !j - 1 in let t = a[!j] in a[!j] <- a[b]; a[b] <- t; assert { exchange (at a 'L) a (!j-1) !j }; decr j done done end
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!