Commit f31fb71f by Asma Tafat-Bouzid

vacid binary heap

 ... ... @@ -2,9 +2,9 @@ theory Elements use import int.Int use import bag.Bag use import map.Map as A use export map.Map type array 'a = A.map int 'a type array 'a = map int 'a (* [elements a i j] is the bag of elements in a[i..j[ *) function elements (a:array 'a) (i j:int) : bag 'a ... ... @@ -14,11 +14,11 @@ axiom Elements_empty : forall a:array 'a, i j:int. axiom Elements_add : forall a:array 'a, i j :int. i < j -> (elements a i j) = (add (A.get a (j-1)) (elements a i (j-1))) (elements a i j) = (add a[j-1] (elements a i (j-1))) lemma Elements_singleton : forall a:array 'a, i j:int. j = i + 1 -> (elements a i j) = (singleton (A.get a i)) (elements a i j) = (singleton a[i]) lemma Elements_union : forall a:array 'a, i j k:int. i <= j <= k -> ... ... @@ -26,11 +26,11 @@ lemma Elements_union : forall a:array 'a, i j k:int. lemma Elements_add1 : forall a:array 'a, i j :int. i < j -> (elements a i j) = (add (A.get a i) (elements a (i+1) j)) (elements a i j) = (add a[i] (elements a (i+1) j)) lemma Elements_remove_last: forall a:array 'a, i j :int. i < j-1 -> (elements a i (j-1)) = diff (elements a i j) (singleton (A.get a (j-1))) (elements a i (j-1)) = diff (elements a i j) (singleton a[j-1]) lemma Occ_elements: forall a:array 'a, i j n:int. i <= j < n -> ... ... @@ -38,22 +38,22 @@ lemma Occ_elements: forall a:array 'a, i j n:int. lemma Elements_set_outside : forall a:array 'a, i j:int. i <= j -> forall k : int. (k < i || k >= j) -> forall e:'a. (elements (A.set a k e) i j) = (elements a i j) forall e:'a. (elements (a[k <- e]) i j) = (elements a i j) lemma Elements_set_inside : forall a:array 'a, i j n: int, e:'a, b:bag 'a. i <= j < n -> (elements a i n) = add (A.get a j) b -> (elements (A.set a j e) i n) = add e b (elements a i n) = add a[j] b -> (elements (a[j <- e]) i n) = add e b lemma Elements_set_inside2 : forall a:array 'a, i j n: int, e:'a. i <= j < n -> elements (A.set a j e) i n = elements a[j <- e] i n = add e (diff (elements a i n) (singleton (a[j]))) end (* Local Variables: compile-command: "why3ide -I . proofs" compile-command: "why3ide -I . elements" End: *) *) \ No newline at end of file
 ... ... @@ -23,7 +23,7 @@ predicate parentChild (i: int) (j: int) = 0 <= i < j -> (j = left i) || (j = right i) use map.Map as A use import map.Map as A type map = A.map int int type logic_heap = (map, int) ... ... @@ -31,7 +31,7 @@ predicate is_heap_array (a: map) (idx: int) (sz: int) = 0 <= idx -> forall i j: int. idx <= i < j < sz -> parentChild i j -> A.get a i <= A.get a j a[i] <= a[j] predicate is_heap (h : logic_heap) = let (a, sz) = h in sz >= 0 /\ is_heap_array a 0 sz ... ... @@ -52,37 +52,37 @@ lemma Is_heap_sub2 : lemma Is_heap_when_node_modified : forall a:map, n e idx i:int. 0 <= i < n -> is_heap_array a idx n -> (i > 0 -> A.get a (parent i) <= e ) -> (left i < n -> e <= A.get a (left i)) -> (right i < n -> e <= A.get a (right i)) -> is_heap_array (A.set a i e) idx n (i > 0 -> a[parent i] <= e ) -> (left i < n -> e <= a[left i]) -> (right i < n -> e <= a[right i]) -> is_heap_array (a[i <- e]) idx n lemma Is_heap_add_last : forall a:map, n e:int. n > 0 -> is_heap_array a 0 n /\ (e >= A.get a (parent n)) -> is_heap_array (A.set a n e) 0 (n + 1) is_heap_array a 0 n /\ (e >= a[parent n]) -> is_heap_array (a[n <- e]) 0 (n + 1) lemma Parent_inf_el: forall a: map, n: int. is_heap_array a 0 n -> forall j:int. 0 < j < n -> A.get a (parent j) <= A.get a j forall j:int. 0 < j < n -> a[parent j] <= a[j] lemma Left_sup_el: forall a: map, n: int. is_heap_array a 0 n -> forall j: int. 0 <= j < n -> left j < n -> A.get a j <= A.get a (left j) a[j] <= a[left j] lemma Right_sup_el: forall a: map, n: int. is_heap_array a 0 n -> forall j: int. 0 <= j < n -> right j < n -> A.get a j <= A.get a (right j) a[j] <= a[right j] lemma Is_heap_relation: forall a:map, n :int. n > 0 -> is_heap_array a 0 n -> forall j: int. 0 <= j -> j < n -> A.get a 0 <= A.get a j forall j: int. 0 <= j -> j < n -> a[0] <= a[j] end ... ...
 ... ... @@ -3,12 +3,12 @@ module Implementation use import int.Int use import int.ComputerDivision use import map.Map (*use import map.Map*) use import heap.Heap use import heap_model.Model use import bag_of_integers.Bag_integers use import elements.Elements use import heap.Heap lemma Is_heap_min: forall a:map, n :int. n > 0 -> ... ... @@ -40,18 +40,18 @@ let insert (this : ref logic_heap) (e : int) : unit = (!i < n -> is_heap_array !arr 0 (n + 1) /\ !arr[!i] > e /\ model (!arr, n+1) = add (A.get !arr !i) (model (a, n))) model (!arr, n+1) = add !arr[!i] (model (a, n))) } variant { !i } let parent = div (!i - 1) 2 in let p = A.get !arr parent in if (e >= p) then raise Break; arr := A.set !arr !i p; arr := !arr[!i<-p]; i := parent done with Break -> () end; arr := A.set !arr !i e; arr := !arr[!i<-e]; this := (!arr, n + 1); assert { 0 < !i < n -> is_heap !this }; assert { !i < n -> model !this = add e (model (a,n)) } ... ...
 theory Model use import int.Int (*use import map.Map*) use import bag.Bag use import elements.Elements ... ... @@ -13,23 +13,22 @@ function model (h:logic_heap): (bag int) = lemma Model_empty : forall a: array int. model (a,0) = empty_bag lemma Model_singleton : forall a: array int. model (a,1) = singleton(A.get a 0) lemma Model_singleton : forall a: array int. model (a,1) = singleton(a[0]) lemma Model_set : forall a a': array int,v: int, i n : int. 0 <= i < n -> a' = A.set a i v -> add (A.get a i) (model (a',n)) = add (a[i]) (model (a[i <- v],n)) = add v (model (a, n)) lemma Model_add_last: forall a: array int, n : int. n >= 0 -> model (a, n+1) = add (A.get a n) (model (a, n)) model (a, n+1) = add (a[n]) (model (a, n)) end (* Local Variables: compile-command: "why3ide -I . proofs" compile-command: "why3ide -I . heap_model.why" End: *)
 ... ... @@ -53,7 +53,7 @@ end (* Local Variables: compile-command: "why3ide -I . proofs" compile-command: "why3ide -I . heapsort.mlw" End: *) ... ...
 ... ... @@ -231,6 +231,4 @@ rewrite <- Union_assoc. apply f_equal. apply Union_comm. Qed. (* DO NOT EDIT BELOW *) (* DO NOT EDIT BELOW *) \ No newline at end of file
 ... ... @@ -221,6 +221,4 @@ destruct h. apply f_equal2; auto. apply H_induc;intuition. Qed. (* DO NOT EDIT BELOW *) (* DO NOT EDIT BELOW *) \ No newline at end of file
 ... ... @@ -206,6 +206,4 @@ generalize (occ_non_negative X (elements a i j) (get a j)). generalize (occ_non_negative X (elements a (j+1)n) (get a j)). omega. Qed. (* DO NOT EDIT BELOW *) (* DO NOT EDIT BELOW *) \ No newline at end of file
 ... ... @@ -209,32 +209,32 @@ Axiom Elements_set_inside2 : forall (a:Type), forall (a1:(map Z a)) (i:Z) Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\ (x <= y)%Z). Definition left(i:Z): Z := ((2%Z * i)%Z + 1%Z)%Z. Definition left1(i:Z): Z := ((2%Z * i)%Z + 1%Z)%Z. Definition right(i:Z): Z := ((2%Z * i)%Z + 2%Z)%Z. Definition right1(i:Z): Z := ((2%Z * i)%Z + 2%Z)%Z. Definition parent(i:Z): Z := (ZOdiv (i - 1%Z)%Z 2%Z). Axiom Parent_inf : forall (i:Z), (0%Z < i)%Z -> ((parent i) < i)%Z. Axiom Left_sup : forall (i:Z), (0%Z <= i)%Z -> (i < (left i))%Z. Axiom Left_sup : forall (i:Z), (0%Z <= i)%Z -> (i < (left1 i))%Z. Axiom Right_sup : forall (i:Z), (0%Z <= i)%Z -> (i < (right i))%Z. Axiom Right_sup : forall (i:Z), (0%Z <= i)%Z -> (i < (right1 i))%Z. Axiom Parent_right : forall (i:Z), (0%Z <= i)%Z -> ((parent (right i)) = i). Axiom Parent_right : forall (i:Z), (0%Z <= i)%Z -> ((parent (right1 i)) = i). Axiom Parent_left : forall (i:Z), (0%Z <= i)%Z -> ((parent (left i)) = i). Axiom Parent_left : forall (i:Z), (0%Z <= i)%Z -> ((parent (left1 i)) = i). Axiom Inf_parent : forall (i:Z) (j:Z), ((0%Z < j)%Z /\ (j <= (right i))%Z) -> ((parent j) <= i)%Z. (j <= (right1 i))%Z) -> ((parent j) <= i)%Z. Axiom Child_parent : forall (i:Z), (0%Z < i)%Z -> ((i = (left (parent i))) \/ (i = (right (parent i)))). ((i = (left1 (parent i))) \/ (i = (right1 (parent i)))). Axiom Parent_pos : forall (j:Z), (0%Z < j)%Z -> (0%Z <= (parent j))%Z. Definition parentChild(i:Z) (j:Z): Prop := ((0%Z <= i)%Z /\ (i < j)%Z) -> ((j = (left i)) \/ (j = (right i))). ((j = (left1 i)) \/ (j = (right1 i))). Definition map1 := (map Z Z). ... ... @@ -260,9 +260,9 @@ Axiom Is_heap_sub2 : forall (a:(map Z Z)) (n:Z), (is_heap_array a 0%Z n) -> Axiom Is_heap_when_node_modified : forall (a:(map Z Z)) (n:Z) (e:Z) (idx:Z) (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((is_heap_array a idx n) -> (((0%Z < i)%Z -> ((get a (parent i)) <= e)%Z) -> ((((left i) < n)%Z -> (e <= (get a (left i)))%Z) -> ((((right i) < n)%Z -> (e <= (get a (right i)))%Z) -> (is_heap_array (set a i e) idx n))))). (((0%Z < i)%Z -> ((get a (parent i)) <= e)%Z) -> ((((left1 i) < n)%Z -> (e <= (get a (left1 i)))%Z) -> ((((right1 i) < n)%Z -> (e <= (get a (right1 i)))%Z) -> (is_heap_array (set a i e) idx n))))). Axiom Is_heap_add_last : forall (a:(map Z Z)) (n:Z) (e:Z), (0%Z < n)%Z -> (((is_heap_array a 0%Z n) /\ ((get a (parent n)) <= e)%Z) -> ... ... @@ -273,12 +273,12 @@ Axiom Parent_inf_el : forall (a:(map Z Z)) (n:Z), (is_heap_array a 0%Z n) -> j))%Z. Axiom Left_sup_el : forall (a:(map Z Z)) (n:Z), (is_heap_array a 0%Z n) -> forall (j:Z), ((0%Z <= j)%Z /\ (j < n)%Z) -> (((left j) < n)%Z -> ((get a j) <= (get a (left j)))%Z). forall (j:Z), ((0%Z <= j)%Z /\ (j < n)%Z) -> (((left1 j) < n)%Z -> ((get a j) <= (get a (left1 j)))%Z). Axiom Right_sup_el : forall (a:(map Z Z)) (n:Z), (is_heap_array a 0%Z n) -> forall (j:Z), ((0%Z <= j)%Z /\ (j < n)%Z) -> (((right j) < n)%Z -> ((get a j) <= (get a (right j)))%Z). forall (j:Z), ((0%Z <= j)%Z /\ (j < n)%Z) -> (((right1 j) < n)%Z -> ((get a j) <= (get a (right1 j)))%Z). Axiom Is_heap_relation : forall (a:(map Z Z)) (n:Z), (0%Z < n)%Z -> ((is_heap_array a 0%Z n) -> forall (j:Z), (0%Z <= j)%Z -> ((j < n)%Z -> ... ... @@ -299,13 +299,12 @@ Axiom Model_singleton : forall (a:(map Z Z)), ((model (a, (* DO NOT EDIT BELOW *) Theorem Model_set : forall (a:(map Z Z)) (aqt:(map Z Z)) (v:Z) (i:Z) (n:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((aqt = (set a i v)) -> ((add (get a i) (model (aqt, n))) = (add v (model (a, n))))). Theorem Model_set : forall (a:(map Z Z)) (v:Z) (i:Z) (n:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((add (get a i) (model ((set a i v), n))) = (add v (model ( a, n)))). (* YOU MAY EDIT THE PROOF BELOW *) intros a a0 v i n H_i H_a0. intros a v i n H_is. unfold model in *. subst a0. rewrite Elements_union with (i:= 0) (j:=i) (k:=n); auto with *. pattern (elements (set a i v) 0 i); rewrite Elements_set_outside; auto with *. rewrite Elements_add1 with (i:= i) (j:=n); auto with *. ... ...
This diff is collapsed.
 module TestHarness (**** logic declarations *****) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!