binomial heaps: proof completed

parent 92ce25c8
......@@ -2,7 +2,7 @@
(** Binomial heaps (Jean Vuillemin, 1978).
Purely applicative implementation, following Okasaki's implementation
in Purely Functional Data Structures (Section 3.2).
in his book "Purely Functional Data Structures" (Section 3.2).
Author: Jean-Christophe Filliâtre (CNRS)
*)
......@@ -40,8 +40,13 @@ module BinomialHeap
| Cons { children = c } r -> 1 + size c + size r
end
lemma size_nonnneg:
forall l. size l >= 0
let lemma size_nonnneg (l: list tree)
ensures { size l >= 0 }
= let rec auxl (l: list tree) ensures { size l >= 0 } variant { l }
= match l with Nil -> () | Cons t r -> auxt t; auxl r end
with auxt (t: tree) ensures { size t.children >= 0 } variant { t }
= match t with { children = c } -> auxl c end in
auxl l
(** Heaps. *)
......
......@@ -6,8 +6,9 @@
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../binomial_heap.mlw" expanded="true">
<theory name="BinomialHeap" sum="8eac636d5b2ef3198243fe3fccc449ba" expanded="true">
<goal name="size_nonnneg" expanded="true">
<theory name="BinomialHeap" sum="69f761ca58435723990c69900429c264" expanded="true">
<goal name="WP_parameter size_nonnneg" expl="VC for size_nonnneg">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="le_roots_trans">
<transf name="induction_ty_lex">
......@@ -528,7 +529,7 @@
</goal>
</transf>
</goal>
<goal name="heap_size" expanded="true">
<goal name="heap_size">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
......
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