gallery: new example tree_height

examples/tree_height.mlw

+
+(** Computing the height of a tree in CPS style
+    (author: Jean-Christophe Filliâtre) *)
+
+module HeightCPS
+
+  use import int.Int
+  use import int.MinMax
+  use import bintree.Tree
+  use import bintree.Height
+  use HighOrd
+
+  function height_cps (t: tree 'a) (k: int -> 'b) : 'b =
+    match t with
+    | Empty -> k 0
+    | Node l _ r ->
+        height_cps l (\ hl.
+        height_cps r (\ hr.
+        k (1 + max hl hr)))
+    end
+
+  function height1 (t: tree 'a) : int = height_cps t (\ h. h)
+
+  lemma height_cps_correct:
+    forall t: tree 'a, k: int -> 'b. height_cps t k = k (height t)
+
+  lemma height1_correct:
+    forall t: tree 'a. height1 t = height t
+
+end
+
+(** Computing the height of a tree with an explicit stack
+    (code: Andrei Paskevich / proof: Jean-Christophe Filliâtre) *)
+
+module HeightStack
+
+  use import int.Int
+  use import int.MinMax
+  use import list.List
+  use import bintree.Tree
+  use import bintree.Size
+  use import bintree.Height
+
+  type stack 'a = list (int, tree 'a)
+
+  function heights (s: stack 'a) : int =
+    match s with
+    | Nil            -> 0
+    | Cons (h, t) s' -> max (h + height t) (heights s')
+    end
+
+  function sizes (s: stack 'a) : int =
+    match s with
+    | Nil            -> 0
+    | Cons (_, t) s' -> size t + sizes s'
+    end
+
+  lemma sizes_nonneg: forall s: stack 'a. sizes s >= 0
+
+  let rec height_stack (m: int) (s: stack 'a) : int
+    requires { m >= 0 }
+    variant  { sizes s, s }
+    ensures  { result = max m (heights s) }
+  = match s with
+    | Nil                     -> m
+    | Cons (h, Empty) s'      -> height_stack (max m h) s'
+    | Cons (h, Node l _ r) s' -> height_stack m (Cons (h+1,l) (Cons (h+1,r) s'))
+   end
+
+  let height1 (t: tree 'a) : int
+    ensures { result = height t }
+  = height_stack 0 (Cons (0, t) Nil)
+
+end

examples/tree_height/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
+<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">
+<theory name="HeightCPS" sum="bf5f8a1bb7474cc558d4defd10f63945">
+ <goal name="height_cps_correct">
+ <transf name="induction_ty_lex">
+  <goal name="height_cps_correct.1" expl="1.">
+  <proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="height1_correct">
+ <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
+ </goal>
+</theory>
+<theory name="HeightStack" sum="9eefeb26becfef0638674737a4335571">
+ <goal name="sizes_nonneg">
+ <transf name="induction_ty_lex">
+  <goal name="sizes_nonneg.1" expl="1.">
+  <proof prover="3"><result status="valid" time="0.10"/></proof>
+  <proof prover="4"><result status="valid" time="0.23"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="WP_parameter height_stack" expl="VC for height_stack">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter height_stack.1" expl="1. postcondition">
+  <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
+  </goal>
+  <goal name="WP_parameter height_stack.2" expl="2. variant decrease">
+  <proof prover="0"><result status="valid" time="0.00" steps="36"/></proof>
+  </goal>
+  <goal name="WP_parameter height_stack.3" expl="3. precondition">
+  <proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
+  </goal>
+  <goal name="WP_parameter height_stack.4" expl="4. postcondition">
+  <proof prover="1"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="WP_parameter height_stack.5" expl="5. variant decrease">
+  <proof prover="0"><result status="valid" time="0.02" steps="51"/></proof>
+  </goal>
+  <goal name="WP_parameter height_stack.6" expl="6. precondition">
+  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+  </goal>
+  <goal name="WP_parameter height_stack.7" expl="7. postcondition">
+  <proof prover="1"><result status="valid" time="0.04"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="WP_parameter height1" expl="VC for height1">
+ <proof prover="1"><result status="valid" time="0.02"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>