tree_height example: third implementation

parent ac867b29
......@@ -29,6 +29,79 @@ module HeightCPS
end
(** with a while loop, manually obtained by compiling out recursion *)
module Iteration
use import int.Int
use import int.MinMax
use import list.List
use import bintree.Tree
use import bintree.Size
use import bintree.Height
use import ref.Ref
type cont 'a = Id | Kleft (tree 'a) (cont 'a) | Kright int (cont 'a)
type what 'a = Argument (tree 'a) | Result int
predicate is_id (k: cont 'a) =
match k with Id -> true | _ -> false end
predicate is_result (w: what 'a) =
match w with Result _ -> true | _ -> false end
function evalk (k: cont 'a) (r: int) : int =
match k with
| Id -> r
| Kleft l k -> evalk k (1 + max (height l) r)
| Kright x k -> evalk k (1 + max x r)
end
function evalw (w: what 'a) : int =
match w with
| Argument t -> height t
| Result x -> x
end
function sizek (k: cont 'a) : int =
match k with
| Id -> 0
| Kleft t k -> 3 + 4 * size t + sizek k
| Kright _ k -> 1 + sizek k
end
lemma sizek_nonneg: forall k: cont 'a. sizek k >= 0
function sizew (w: what 'a) : int =
match w with
| Argument t -> 1 + 4 * size t
| Result _ -> 0
end
lemma helper1: forall t: tree 'a. 4 * size t >= 0
lemma sizew_nonneg: forall w: what 'a. sizew w >= 0
let height1 (t: tree 'a) : int
ensures { result = height t }
=
let w = ref (Argument t) in
let k = ref Id in
while not (is_id !k && is_result !w) do
invariant { evalk !k (evalw !w) = height t }
variant { sizek !k + sizew !w }
match !w, !k with
| Argument Empty, _ -> w := Result 0
| Argument (Node l _ r), _ -> w := Argument l; k := Kleft r !k
| Result _, Id -> absurd
| Result v, Kleft r k0 -> w := Argument r; k := Kright v k0
| Result v, Kright hl k0 -> w := Result (1 + max hl v); k := k0
end
done;
match !w with Result r -> r | _ -> absurd end
end
(** Computing the height of a tree with an explicit stack
(code: Andrei Paskevich / proof: Jean-Christophe Filliâtre) *)
......@@ -72,3 +145,4 @@ module HeightStack
= height_stack 0 (Cons (0, t) Nil)
end
......@@ -6,7 +6,7 @@
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="6" memlimit="1000"/>
<prover id="4" name="Vampire" version="0.6" timelimit="6" memlimit="1000"/>
<file name="../tree_height.mlw">
<file name="../tree_height.mlw" expanded="true">
<theory name="HeightCPS" sum="bf5f8a1bb7474cc558d4defd10f63945">
<goal name="height_cps_correct">
<transf name="induction_ty_lex">
......@@ -19,6 +19,136 @@
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
</theory>
<theory name="Iteration" sum="2c31a081b486a7999a2cf635e7cb3b2c" expanded="true">
<goal name="sizek_nonneg">
<transf name="induction_ty_lex">
<goal name="sizek_nonneg.1" expl="1.">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
</goal>
<goal name="helper1">
<proof prover="0"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="sizew_nonneg">
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="WP_parameter height1" expl="VC for height1" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter height1.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter height1.2" expl="2. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="WP_parameter height1.3" expl="3. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter height1.4" expl="4. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="WP_parameter height1.5" expl="5. loop variant decrease">
<proof prover="0"><result status="valid" time="0.04" steps="56"/></proof>
</goal>
<goal name="WP_parameter height1.6" expl="6. unreachable point">
<proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter height1.7" expl="7. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="36"/></proof>
</goal>
<goal name="WP_parameter height1.8" expl="8. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter height1.9" expl="9. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="39"/></proof>
</goal>
<goal name="WP_parameter height1.10" expl="10. loop variant decrease">
<proof prover="0"><result status="valid" time="0.04" steps="36"/></proof>
</goal>
<goal name="WP_parameter height1.11" expl="11. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="WP_parameter height1.12" expl="12. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter height1.13" expl="13. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03" steps="34"/></proof>
</goal>
<goal name="WP_parameter height1.14" expl="14. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter height1.15" expl="15. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="WP_parameter height1.16" expl="16. loop variant decrease">
<proof prover="0"><result status="valid" time="0.04" steps="34"/></proof>
</goal>
<goal name="WP_parameter height1.17" expl="17. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter height1.18" expl="18. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter height1.19" expl="19. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="12"/></proof>
</goal>
<goal name="WP_parameter height1.20" expl="20. unreachable point">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter height1.21" expl="21. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
<goal name="WP_parameter height1.22" expl="22. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter height1.23" expl="23. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="59"/></proof>
</goal>
<goal name="WP_parameter height1.24" expl="24. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="83"/></proof>
</goal>
<goal name="WP_parameter height1.25" expl="25. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="WP_parameter height1.26" expl="26. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
<goal name="WP_parameter height1.27" expl="27. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter height1.28" expl="28. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="WP_parameter height1.29" expl="29. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="80"/></proof>
</goal>
<goal name="WP_parameter height1.30" expl="30. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="WP_parameter height1.31" expl="31. loop variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter height1.32" expl="32. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
<goal name="WP_parameter height1.33" expl="33. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter height1.34" expl="34. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03" steps="65"/></proof>
</goal>
<goal name="WP_parameter height1.35" expl="35. loop variant decrease">
<proof prover="0"><result status="valid" time="0.03" steps="90"/></proof>
</goal>
<goal name="WP_parameter height1.36" expl="36. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="WP_parameter height1.37" expl="37. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="HeightStack" sum="9eefeb26becfef0638674737a4335571">
<goal name="sizes_nonneg">
<transf name="induction_ty_lex">
......
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