Heap implementation

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 ==="

examples/programs/vacid_0_binary_heaps/heap.why

+
+
+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:
+*)

examples/programs/vacid_0_binary_heaps/heap_implem.mlw

+
+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:
+*)

examples/programs/vacid_0_binary_heaps/heap_model.why

+
+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:
+*)