From 68b48a25cbf8a8aa29e5131dd39555f42776a40e Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Sun, 17 Jul 2011 09:41:54 +0200
Subject: [PATCH] Heap implementation
---
bench/bench | 7 +-
.../programs/vacid_0_binary_heaps/heap.why | 94 ++++++++++++++
.../vacid_0_binary_heaps/heap_implem.mlw | 116 ++++++++++++++++++
.../vacid_0_binary_heaps/heap_model.why | 35 ++++++
4 files changed, 249 insertions(+), 3 deletions(-)
create mode 100644 examples/programs/vacid_0_binary_heaps/heap.why
create mode 100644 examples/programs/vacid_0_binary_heaps/heap_implem.mlw
create mode 100644 examples/programs/vacid_0_binary_heaps/heap_model.why
diff --git a/bench/bench b/bench/bench
index e048a9296b..0b7d1907a2 100755
--- a/bench/bench
+++ b/bench/bench
@@ -58,10 +58,10 @@ drivers () {
programs () {
for f in $1/*.mlw; do
echo -n " "$f"... "
- if ! $pgml -L modules $pgml_options $f > /dev/null 2>&1; then
+ if ! $pgml -L modules $pgml_options $f $2 > /dev/null 2>&1; then
echo
- echo "$pgml $pgml_options $f"
- $pgml -L modules $pgml_options $f
+ echo "$pgml $pgml_options $f $2"
+ $pgml -L modules $pgml_options $f $2
echo "FAILED!"
exit 1
else
@@ -147,6 +147,7 @@ echo "=== VC generation on good programs ==="
pgml_options=
programs bench/programs/good
programs examples/programs
+programs examples/programs/vacid_0_binary_heaps "-I examples/programs/vacid_0_binary_heaps"
echo ""
echo "=== Checking valid goals ==="
diff --git a/examples/programs/vacid_0_binary_heaps/heap.why b/examples/programs/vacid_0_binary_heaps/heap.why
new file mode 100644
index 0000000000..b08cde60a2
--- /dev/null
+++ b/examples/programs/vacid_0_binary_heaps/heap.why
@@ -0,0 +1,94 @@
+
+
+theory Heap
+
+use import int.Int
+use import int.ComputerDivision
+
+function left(i:int) : int = 2*i+1
+function right(i:int) : int = 2*i+2
+function parent(i:int) : int = div (i-1) 2
+
+lemma Parent_inf: forall i:int. 0 < i -> parent i < i
+lemma Left_sup: forall i:int. 0 <= i -> i < left i
+lemma Right_sup: forall i:int. 0 <= i -> i < right i
+lemma Parent_right:forall i:int. 0 <= i -> parent (right i) = i
+lemma Parent_left:forall i:int. 0 <= i -> parent (left i) = i
+lemma Inf_parent: forall i j: int. 0 < j <= right i -> parent j <= i
+lemma Child_parent:forall i:int. 0 < i ->
+ i = left (parent i) || i = right (parent i)
+lemma Parent_pos: forall j: int. 0 < j -> 0 <= parent j
+
+predicate parentChild (i: int) (j: int) =
+ 0 <= i < j -> (j = left i) || (j = right i)
+
+
+use map.Map as A
+type map = A.map int int
+type logic_heap = (map, int)
+
+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
+
+predicate is_heap (h : logic_heap) =
+ let (a, sz) = h in sz >= 0 /\ is_heap_array a 0 sz
+
+lemma Is_heap_when_no_element :
+ forall a:map, idx n: int. 0 <= n <= idx -> is_heap_array a idx n
+
+lemma Is_heap_sub :
+ forall a:map, i n :int.
+ is_heap_array a i n ->
+ forall j: int. i <= j <= n -> is_heap_array a i j
+
+lemma Is_heap_sub2 :
+ forall a:map, n :int.
+ is_heap_array a 0 n ->
+ forall j: int. 0 <= j <= n -> is_heap_array a j n
+
+lemma Is_heap_when_node_modified :
+ forall a:map, n e idx:int.
+ is_heap_array a idx n
+ -> forall i : int. 0 <= i < 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
+
+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)
+
+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
+
+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)
+
+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)
+
+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
+
+end
+
+(*
+Local Variables:
+compile-command: "why3ide -I . vacid0_binary_heaps"
+End:
+*)
diff --git a/examples/programs/vacid_0_binary_heaps/heap_implem.mlw b/examples/programs/vacid_0_binary_heaps/heap_implem.mlw
new file mode 100644
index 0000000000..902f998fb7
--- /dev/null
+++ b/examples/programs/vacid_0_binary_heaps/heap_implem.mlw
@@ -0,0 +1,116 @@
+
+module Implementation
+
+use import int.Int
+use import int.ComputerDivision
+use import heap.Heap
+use import heap_model.Model
+use import bag_of_integers.Bag_integers
+
+lemma Is_heap_min:
+ forall a:map, n :int. n > 0 ->
+ is_heap_array a 0 n -> A.get a 0 = min_bag (model (a, n))
+
+use import module ref.Ref
+
+(* implementation of heaps *)
+let create () : ref logic_heap =
+ { true }
+ let x = (A.const 0, 0) in ref x
+ { is_heap !result /\
+ model !result = empty_bag }
+
+exception Break
+
+let insert (this : ref logic_heap) (e : int) : unit =
+{ is_heap !this }
+ let (a, n) = !this in
+ let arr = ref a in
+ let i = ref n in
+ try
+ while (!i > 0) do
+ invariant {
+ 0 <= !i <= n /\
+ (!i = n ->
+ is_heap_array !arr 0 n /\
+ model (!arr, n) = model (a, n)) /\
+ (!i < n ->
+ is_heap_array !arr 0 (n + 1) /\
+ A.get !arr !i > e /\
+ model (!arr, n+1) = add (A.get !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;
+ i := parent;
+ assert { is_heap_array !arr 0 (n + 1) }
+ done
+ with Break -> ()
+ end;
+ arr := A.set !arr !i e;
+ this := (!arr, n + 1);
+ assert { !i = n -> is_heap !this };
+ assert { !i < n -> is_heap !this }
+{ is_heap !this /\
+ model !this = add e (model (old !this)) }
+
+let extractMin (this : ref logic_heap) : int =
+{ model !this <> empty_bag /\ is_heap !this }
+ let (a, n) = !this in
+ assert {n > 0};
+ let arr = ref a in
+ let min = A.get !arr 0 in
+ let n' = n-1 in
+ let last = A.get !arr n' in
+ let i = ref 0 in
+ try
+ while ( !i < n') do
+ invariant {
+ !i >= 0 /\
+ is_heap_array !arr 0 n' /\
+ (!i = 0 ->
+ a = !arr /\
+ (model !this) = add last (model (a, n'))) /\
+ (0 < !i < n' ->
+ add (A.get !arr !i) (model !this) =
+ add last (add min (model (!arr, n')))) /\
+ (!i > 0 -> A.get !arr (parent !i) < last) }
+ variant {n' - !i}
+ let left = 2 * !i + 1 in
+ let right = 2 * !i + 2 in
+ if (left >= n') then raise Break;
+ let smaller = ref left in
+ if right < n' then
+ if A.get !arr left > A.get !arr right
+ then smaller := right;
+ if (last <= (A.get !arr !smaller)) then raise Break;
+ assert {last > (A.get !arr !smaller)};
+ arr := A.set !arr !i (A.get !arr !smaller);
+ i := !smaller
+ done;
+ assert { model !this = add min (model (!arr,n')) }
+ with Break ->
+ assert { add (A.get !arr !i) (model !this) =
+ add last (add min (model (!arr, n'))) }
+ end;
+ if (!i < n') then
+ begin
+ arr := A.set !arr !i last;
+ assert { is_heap_array !arr 0 n' };
+ assert { model !this = add min (model (!arr,n')) }
+ end;
+ this := (!arr, n');
+ min
+{ is_heap !this /\
+ result = min_bag (model (old !this)) /\
+ model (old !this) = add result (model !this) }
+
+end
+
+(*
+Local Variables:
+compile-command: "why3ide -I . vacid0_binary_heaps"
+End:
+*)
diff --git a/examples/programs/vacid_0_binary_heaps/heap_model.why b/examples/programs/vacid_0_binary_heaps/heap_model.why
new file mode 100644
index 0000000000..1b42e1003e
--- /dev/null
+++ b/examples/programs/vacid_0_binary_heaps/heap_model.why
@@ -0,0 +1,35 @@
+
+theory Model
+
+use import int.Int
+
+use import bag.Bag
+use import elements.Elements
+use import heap.Heap
+
+function model (h:logic_heap): (bag int) =
+ let (a,n) = h in elements a 0 n
+
+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_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 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))
+
+end
+
+(*
+Local Variables:
+compile-command: "why3ide -I . vacid0_model_theory"
+End:
+*)
--
GitLab