 ### [library] renamed permut... symbols in map.MapPermut and array.ArrayPermut,

```as follows:

maps:   permut_sub     -> permut
arrays: map_permut_sub -> permut     (to be consistent with maps)
permut_sub     -> permut_sub
permut         -> permut_all```
 * marks an incompatible change * [library] fixed inconsistency in libraries map.MapPermut and array.ArrayPermut; names and meaning of symbols "permut..." have been modified version 0.82, December 12, 2013 =============================== ... ...
 ... ... @@ -50,7 +50,7 @@ module Algo64 end let qs (a:array int) : unit ensures { permut (old a) a } ensures { permut_all (old a) a } ensures { sorted a } = if length a > 0 then quicksort a 0 (length a - 1) ... ...
 ... ... @@ -39,18 +39,18 @@ module FIND let find (a: array int) = requires { length a = _N+1 } ensures { found a /\ permut a (old a) } ensures { found a /\ permut_all a (old a) } '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 } permut_all 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) } termination !i !j !m !n r a /\ permut_all a (at a 'Init) } variant { _N + 2 + !j - !i } 'L: while a[!i] < r do invariant { i_invariant !m !n !i r a /\ ... ...
 ... ... @@ -80,48 +80,48 @@ Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) ((~ (k = i)) -> ((~ (k = j)) -> ((get a1 k) = (get a2 k)))))))). (* Why3 assumption *) Definition map_permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) l u))). (u <= (length a1))%Z) /\ (map.MapPermut.permut (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((map_permut_sub a1 a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u 0%Z l) /\ ((permut a1 a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u (length a1))). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) 0%Z (length a1)). Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut (elts a1) (elts a2) 0%Z (length a1)). Axiom permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut a1 a1). Axiom permut_all_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut_all a1 a1). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut a1 a2). Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut_all a1 a2). Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut a1 a2) -> (permut a2 a1). Axiom permut_all_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut_all a1 a2) -> (permut_all a2 a1). Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). Axiom permut_all_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut_all a1 a2) -> ((permut_all a2 a3) -> (permut_all a1 a3)). Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut a1 a2). Axiom array_eq_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut_all a1 a2). Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z) (u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) -> (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))). Axiom permut_sub_permut : forall {a:Type} {a_WT:WhyType a}, Axiom permut_sub_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut a1 a2). a1 a2 l u) -> (permut_all a1 a2). Parameter usN: Z. ... ... @@ -167,13 +167,13 @@ Import MapPermut. Theorem WP_parameter_find : forall (a:Z) (a1:(@map.Map.map Z _ Z _)), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\ (a = (usN + 1%Z)%Z)) -> forall (n:Z) (m:Z) (a3:(@map.Map.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 -> let o := f in a3) in (((m_invariant m a4) /\ ((n_invariant n a4) /\ ((permut_all a4 a2) /\ ((1%Z <= m)%Z /\ (n <= usN)%Z)))) -> ((m < n)%Z -> let o := f in (((0%Z <= a)%Z /\ ((0%Z <= o)%Z /\ (o < a)%Z)) -> let r := (map.Map.get a3 o) in forall (j:Z) (i:Z) (a5:(@map.Map.map Z _ Z _)), let a6 := (mk_array a a5) in (((i_invariant m n i r a6) /\ ((j_invariant m n j r a6) /\ ((m_invariant m a6) /\ ((n_invariant n a6) /\ ((0%Z <= j)%Z /\ ((i <= (usN + 1%Z)%Z)%Z /\ ((termination i j m n r a6) /\ (permut a6 ((i <= (usN + 1%Z)%Z)%Z /\ ((termination i j m n r a6) /\ (permut_all a6 a2)))))))) -> ((i <= j)%Z -> forall (i1:Z), ((i_invariant m n i1 r a6) /\ (((i <= i1)%Z /\ (i1 <= n)%Z) /\ (termination i1 j m n r a6))) -> (((0%Z <= a)%Z /\ ((0%Z <= i1)%Z /\ (i1 < a)%Z)) -> ((~ ((map.Map.get a5 ... ... @@ -191,7 +191,8 @@ Theorem WP_parameter_find : forall (a:Z) (a1:(@map.Map.map Z _ Z _)), (i2 = (i1 + 1%Z)%Z) -> forall (j2:Z), (j2 = (j1 - 1%Z)%Z) -> ((i_invariant m n i2 r a9) /\ ((j_invariant m n j2 r a9) /\ ((m_invariant m a9) /\ ((n_invariant n a9) /\ ((0%Z <= j2)%Z /\ ((i2 <= (usN + 1%Z)%Z)%Z /\ ((termination i2 j2 m n r a9) /\ (permut a9 a2)))))))))))))))))))))))))))). ((termination i2 j2 m n r a9) /\ (permut_all a9 a2)))))))))))))))))))))))))))). (* Why3 intros a a1 a2 (h1,h2) n m a3 a4 (h3,(h4,(h5,(h6,h7)))) h8 o (h9,(h10,h11)) r j i a5 a6 (h12,(h13,(h14,(h15,(h16,(h17,(h18,h19))))))) h20 i1 ... ... @@ -336,8 +337,8 @@ intuition. red; simpl. split. trivial. apply permut_trans with a5. assert (permut (mk_array a a8) (mk_array a a5)). apply exchange_permut with i1 j1; auto. assert (permut_all (mk_array a a8) (mk_array a a5)). apply exchange_permut_all with i1 j1; auto. destruct H54; intuition. red in H19; intuition. Qed. ... ...
This diff is collapsed.
 ... ... @@ -28,7 +28,7 @@ module Flag monochrome a 0 b Blue /\ monochrome a b r White /\ monochrome a r (length a) Red } ensures { permut (old a) a } ensures { permut_all (old a) a } = let b = ref 0 in let i = ref 0 in ... ... @@ -39,7 +39,7 @@ module Flag invariant { monochrome a 0 !b Blue } invariant { monochrome a !b !i White } invariant { monochrome a !r (length a) Red } invariant { permut (at a 'Init) a } invariant { permut_all (at a 'Init) a } variant { !r - !i } match a[!i] with | Blue -> ... ...
This diff is collapsed.
 ... ... @@ -11,16 +11,16 @@ module InsertionSort use import array.ArrayEq let insertion_sort (a: array int) = ensures { sorted a /\ permut (old a) a } ensures { sorted a /\ permut_all (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 } invariant { sorted_sub a 0 i /\ permut_all (at a 'L) a } let v = a[i] in let j = ref i in while !j > 0 && a[!j - 1] > v do invariant { 0 <= !j <= i } invariant { permut (at a 'L) a[!j <- v] } invariant { permut_all (at a 'L) a[!j <- v] } invariant { forall k1 k2: int. 0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2] } invariant { forall k: int. !j+1 <= k <= i -> v < a[k] } ... ... @@ -86,16 +86,16 @@ module InsertionSortGen M.sorted_sub a.elts 0 a.length let insertion_sort (a: array elt) = ensures { sorted a /\ permut (old a) a } ensures { sorted a /\ permut_all (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 } invariant { sorted_sub a 0 i /\ permut_all (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 { permut_all (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] } ... ...
 ... ... @@ -80,50 +80,48 @@ Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) ((~ (k = i)) -> ((~ (k = j)) -> ((get a1 k) = (get a2 k)))))))). (* Why3 assumption *) Definition map_permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) l u))). (u <= (length a1))%Z) /\ (map.MapPermut.permut (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ ((map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((map.MapPermut.permut_sub (elts a1) (elts a2) l u) /\ (map_eq_sub (elts a2) (elts a2) u (length a1)))))). (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((permut a1 a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u (length a1))). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) 0%Z (length a1)). Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut (elts a1) (elts a2) 0%Z (length a1)). Axiom permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut a1 a1). Axiom permut_all_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut_all a1 a1). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut a1 a2). Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut_all a1 a2). Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut a1 a2) -> (permut a2 a1). Axiom permut_all_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut_all a1 a2) -> (permut_all a2 a1). Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). Axiom permut_all_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut_all a1 a2) -> ((permut_all a2 a3) -> (permut_all a1 a3)). Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut a1 a2). Axiom array_eq_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut_all a1 a2). Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z) (u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) -> (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))). Axiom permut_sub_permut : forall {a:Type} {a_WT:WhyType a}, Axiom permut_sub_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut a1 a2). a1 a2 l u) -> (permut_all a1 a2). Axiom elt : Type. Parameter elt_WhyType : WhyType elt. ... ... @@ -161,21 +159,22 @@ Theorem WP_parameter_insertion_sort : forall (a:Z) (a1:(@map.Map.map Z _ elt elt_WhyType)), let a2 := (mk_array a a1) in ((0%Z <= a)%Z -> let o := (a - 1%Z)%Z in ((1%Z <= o)%Z -> forall (a3:(@map.Map.map Z _ elt elt_WhyType)), forall (i:Z), ((1%Z <= i)%Z /\ (i <= o)%Z) -> (((sorted_sub a3 0%Z i) /\ (permut a2 (mk_array a a3))) -> (((sorted_sub a3 0%Z i) /\ (permut_all a2 (mk_array a a3))) -> (((0%Z <= a)%Z /\ ((0%Z <= i)%Z /\ (i < a)%Z)) -> let v := (map.Map.get a3 i) in forall (j:Z) (a4:(@map.Map.map Z _ elt elt_WhyType)), (((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut a2 (mk_array a (map.Map.set a4 j v))) /\ ((forall (k1:Z) (k2:Z), ((0%Z <= k1)%Z /\ ((k1 <= k2)%Z /\ (k2 <= i)%Z)) -> ((~ (k1 = j)) -> ((~ (k2 = j)) -> (le (map.Map.get a4 k1) (map.Map.get a4 k2))))) /\ forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (le v (map.Map.get a4 k))))) -> ((0%Z < j)%Z -> let o1 := (j - 1%Z)%Z in (((0%Z <= a)%Z /\ ((0%Z <= o1)%Z /\ (o1 < a)%Z)) -> ((~ (le (map.Map.get a4 o1) v)) -> let o2 := (j - 1%Z)%Z in (((0%Z <= o2)%Z /\ (o2 < a)%Z) -> (((0%Z <= j)%Z /\ (j < a)%Z) -> forall (a5:(@map.Map.map Z _ (((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut_all a2 (mk_array a (map.Map.set a4 j v))) /\ ((forall (k1:Z) (k2:Z), ((0%Z <= k1)%Z /\ ((k1 <= k2)%Z /\ (k2 <= i)%Z)) -> ((~ (k1 = j)) -> ((~ (k2 = j)) -> (le (map.Map.get a4 k1) (map.Map.get a4 k2))))) /\ forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (le v (map.Map.get a4 k))))) -> ((0%Z < j)%Z -> let o1 := (j - 1%Z)%Z in (((0%Z <= a)%Z /\ ((0%Z <= o1)%Z /\ (o1 < a)%Z)) -> ((~ (le (map.Map.get a4 o1) v)) -> let o2 := (j - 1%Z)%Z in (((0%Z <= o2)%Z /\ (o2 < a)%Z) -> (((0%Z <= j)%Z /\ (j < a)%Z) -> forall (a5:(@map.Map.map Z _ elt elt_WhyType)), ((0%Z <= a)%Z /\ (a5 = (map.Map.set a4 j (map.Map.get a4 o2)))) -> ((exchange (mk_array a (map.Map.set a4 j v)) (mk_array a (map.Map.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 (map.Map.set a5 j1 (j1 = (j - 1%Z)%Z) -> (permut_all a2 (mk_array a (map.Map.set a5 j1 v))))))))))))). (* Why3 intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4 ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21) ... ... @@ -183,7 +182,7 @@ Theorem WP_parameter_insertion_sort : forall (a:Z) (a1:(@map.Map.map Z _ intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4 ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21) (h22,h23) a5 (h24,h25) h26 j1 h27. unfold permut in *. unfold permut_all in *. simpl; split; auto. simpl in h12. destruct h12 as (h12a & h12b). ... ...
 ... ... @@ -93,50 +93,48 @@ Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) ((~ (k = i)) -> ((~ (k = j)) -> ((get a1 k) = (get a2 k)))))))). (* Why3 assumption *) Definition map_permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) l u))). (u <= (length a1))%Z) /\ (map.MapPermut.permut (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ ((map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((map.MapPermut.permut_sub (elts a1) (elts a2) l u) /\ (map_eq_sub (elts a2) (elts a2) u (length a1)))))). (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((permut a1 a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u (length a1))). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut_sub (elts a1) (elts a2) 0%Z (length a1)). Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut (elts a1) (elts a2) 0%Z (length a1)). Axiom permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut a1 a1). Axiom permut_all_refl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)), (permut_all a1 a1). Axiom exchange_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut a1 a2). Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z), (exchange a1 a2 i j) -> (permut_all a1 a2). Axiom permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut a1 a2) -> (permut a2 a1). Axiom permut_all_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (permut_all a1 a2) -> (permut_all a2 a1). Axiom permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). Axiom permut_all_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (a3:(@array a a_WT)), (permut_all a1 a2) -> ((permut_all a2 a3) -> (permut_all a1 a3)). Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut a1 a2). Axiom array_eq_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)), (array_eq a1 a2) -> (permut_all a1 a2). Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z) (u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) -> (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))). Axiom permut_sub_permut : forall {a:Type} {a_WT:WhyType a}, Axiom permut_sub_permut_all : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut a1 a2). a1 a2 l u) -> (permut_all a1 a2). Import MapPermut. ... ... @@ -145,10 +143,10 @@ Theorem WP_parameter_insertion_sort : forall (a:Z) (a1:(@map.Map.map Z _ Z _)), let a2 := (mk_array a a1) in ((0%Z <= a)%Z -> let o := (a - 1%Z)%Z in ((1%Z <= o)%Z -> forall (a3:(@map.Map.map Z _ Z _)), forall (i:Z), ((1%Z <= i)%Z /\ (i <= o)%Z) -> (((sorted_sub a3 0%Z i) /\ (permut a2 (mk_array a a3))) -> (((0%Z <= a)%Z /\ ((0%Z <= i)%Z /\ (permut_all a2 (mk_array a a3))) -> (((0%Z <= a)%Z /\ ((0%Z <= i)%Z /\ (i < a)%Z)) -> let v := (map.Map.get a3 i) in forall (j:Z) (a4:(@map.Map.map Z _ Z _)), (((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut a2 (mk_array a (map.Map.set a4 j v))) /\ ((forall (k1:Z) (k2:Z), (a4:(@map.Map.map Z _ Z _)), (((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut_all a2 (mk_array a (map.Map.set a4 j v))) /\ ((forall (k1:Z) (k2:Z), ((0%Z <= k1)%Z /\ ((k1 <= k2)%Z /\ (k2 <= i)%Z)) -> ((~ (k1 = j)) -> ((~ (k2 = j)) -> ((map.Map.get a4 k1) <= (map.Map.get a4 k2))%Z))) /\ forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (v < (map.Map.get a4 ... ... @@ -158,7 +156,7 @@ Theorem WP_parameter_insertion_sort : forall (a:Z) (a1:(@map.Map.map Z _ (j < a)%Z) -> forall (a5:(@map.Map.map Z _ Z _)), ((0%Z <= a)%Z /\ (a5 = (map.Map.set a4 j (map.Map.get a4 o2)))) -> ((exchange (mk_array a (map.Map.set a4 j v)) (mk_array a (map.Map.set a5 (j - 1%Z)%Z v)) (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut a2 (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut_all a2 (mk_array a (map.Map.set a5 j1 v))))))))))))). (* Why3 intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4 ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21) ... ... @@ -167,7 +165,7 @@ intros a a1 a2 h1 o h2 a3 i (h3,h4) (h5,h6) (h7,(h8,h9)) v j a4 ((h10,h11),(h12,(h13,h14))) h15 o1 (h16,(h17,h18)) h19 o2 (h20,h21) (h22,h23) a5 (h24,h25) h26 j1 h27. intuition. unfold permut. unfold permut_all. split. simpl. auto. ... ... @@ -175,10 +173,10 @@ subst a5. simpl. apply permut_trans with (elts (set (mk_array a a4) j (Map.get a3 i))); auto. subst j1. unfold permut in h12. unfold permut_all in h12. intuition. generalize (exchange_permut _ _ _ _ h26). unfold permut; simpl; intuition. generalize (exchange_permut_all _ _ _ _ h26). unfold permut_all; simpl; intuition. subst j1; assumption. Qed.
This diff is collapsed.
 ... ... @@ -17,16 +17,16 @@ module InsertionSortNaive let sort (a:array int) ensures { sorted a } ensures { permut (old a) a } ensures { permut_all (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut (at a 'Init) a } invariant { permut_all (at a 'Init) a } invariant { sorted_sub a 0 i } let j = ref i in while !j > 0 && a[!j-1] > a[!j] do invariant { 0 <= !j <= i } invariant { permut (at a 'Init) a } invariant { permut_all (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 -> ... ... @@ -70,16 +70,16 @@ module InsertionSortNaiveGen let sort (a:array elt) ensures { sorted a } ensures { permut (old a) a } ensures { permut_all (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut (at a 'Init) a } invariant { permut_all (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 { permut_all (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 -> ... ... @@ -130,16 +130,16 @@ module InsertionSortParam let sort (p:param) (a:array elt) ensures { sorted p a } ensures { permut (old a) a } ensures { permut_all (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut (at a 'Init) a } invariant { permut_all (at a 'Init) a } invariant { sorted_sub p a.elts 0 i } let j = ref i in while !j > 0 && not (le p a[!j-1] a[!j]) do invariant { 0 <= !j <= i } invariant { permut (at a 'Init) a } invariant { permut_all (at a 'Init) a } invariant { sorted_sub p a.elts 0 !j } invariant { sorted_sub p a.elts !j (i+1) } invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i -> ... ... @@ -191,16 +191,16 @@ module InsertionSortParamBad let sort (p:param) (a:array elt) ensures { sorted p a } ensures { permut (old a) a } ensures { permut_all (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut (at a 'Init) a } invariant { permut_all (at a 'Init) a } invariant { sorted_sub p a 0 i } let j = ref i in while !j > 0 && not (le p a[!j-1] a[!j]) do invariant { 0 <= !j <= i } invariant { permut (at a 'Init) a } invariant { permut_all (at a 'Init) a } invariant { sorted_sub p a 0 !j } invariant { sorted_sub p a !j (i+1) } invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i -> ... ...
This source diff could not be displayed because it is too large. You can view the blob instead.
 ... ... @@ -34,7 +34,7 @@ module Quicksort end let quicksort (t : array int) = ensures { sorted t /\ permut (old t) t } ensures { sorted t /\ permut_all (old t) t } quick_rec t 0 (length t - 1) ... ...
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -12,12 +12,12 @@ module SelectionSort use import array.ArrayEq let selection_sort (a: array int) ensures { sorted a /\ permut (old a) a } = ensures { sorted a /\ permut_all (old a) a } = 'L: let min = ref 0 in for i = 0 to length a - 1 do (* a[0..i[ is sorted; now find minimum of a[i..n[ *) invariant { sorted_sub a 0 i /\ permut (at a 'L) a /\ invariant { sorted_sub a 0 i /\ permut_all (at a 'L) a /\ forall k1 k2: int. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] } (* let min = ref i in *) min := i; for j = i + 1 to length a - 1 do ... ... @@ -27,7 +27,7 @@ module SelectionSort done; 'L1: if !min <> i then swap a !min i; assert { permut (at a 'L1) a } assert { permut_all (at a 'L1) a } done let test1 () = ... ...
This diff is collapsed.
 ... ... @@ -257,18 +257,18 @@ let sort (a:array int) (data : array int) requires { data.length = a.length } requires { range data } ensures { sorted a data } ensures { ArrayPermut.permut (old data) data } ensures { ArrayPermut.permut_all (old data) data } = 'Init: for i = 0 to data.length - 1 do invariant { ArrayPermut.permut (at data 'Init) data } invariant { ArrayPermut.permut_all (at data 'Init) data } invariant { sorted_sub a data.elts 0 i } invariant { range data } let j = ref i in while !j > 0 && compare a data[!j-1] data[!j] > 0 do invariant { 0 <= !j <= i } invariant { range data } invariant { ArrayPermut.permut (at data 'Init) data } invariant { ArrayPermut.permut_all (at data 'Init) data } invariant { sorted_sub a data.elts 0 !j } invariant { sorted_sub a data.elts !j (i+1) } invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i -> ... ... @@ -353,7 +353,7 @@ use array.ArrayPermut (** needed to establish invariant in function [create] *) lemma permut_permutation : forall a1 a2:array int. ArrayPermut.permut a1 a2 /\ permutation a1.elts a1.length -> ArrayPermut.permut_all a1 a2 /\ permutation a1.elts a1.length -> permutation a2.elts a2.length (** constructor of suffixArray structure *) ... ...
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -20,13 +20,13 @@ module TwoWaySort