Commit bb11c2df authored by MARCHE Claude's avatar MARCHE Claude

proof in progress: heap_implem.extractMin

parent f5583575
......@@ -50,13 +50,12 @@ lemma Is_heap_sub2 :
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
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
lemma Is_heap_add_last :
forall a:map, n e:int. n > 0 ->
......
......@@ -97,6 +97,7 @@ let extractMin (this : ref logic_heap) : int =
if (!i < n') then
begin
arr := A.set !arr !i last;
assert { !i > 0 -> is_heap_array !arr 0 n' };
assert { is_heap_array !arr 0 n' };
assert { model !this = add min (model (!arr,n')) }
end;
......
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment