foveoos11_challenge2: added proof of termination

examples/programs/foveoos11_challenge2.mlw

@@ -12,12 +12,19 @@ module MaximumTree
 
   type tree = Empty | Node tree int tree
 
+  function size (t: tree) : int = match t with
+    | Empty      -> 0
+    | Node l _ r -> 1 + size l + size r
+  end
+
+  lemma size_nonneg: forall t: tree. size t >= 0
+
   predicate mem (x: int) (t: tree) = match t with
     | Empty      -> false
     | Node l v r -> mem x l \/ x = v \/ mem x r
   end
 
-  let rec maximum (t: tree) : int =
+  let rec maximum (t: tree) : int variant { size t } =
     { t <> Empty }
     match t with
       | Empty              -> absurd

examples/programs/foveoos11_challenge2/foveoos11_challenge2_WP_MaximumTree_size_nonneg_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Definition unit  := unit.
+
+Parameter qtmark : Type.
+
+Parameter at1: forall (a:Type), a -> qtmark -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a -> a.
+
+Implicit Arguments old.
+
+Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\
+  (y <= (Zmax x y))%Z.
+
+Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y).
+
+Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\
+  ((Zmin x y) <= y)%Z.
+
+Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y).
+
+Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x).
+
+Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y).
+
+Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x).
+
+Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y).
+
+Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)).
+
+Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)).
+
+Inductive tree  :=
+  | Empty : tree 
+  | Node : tree -> Z -> tree -> tree .
+
+Set Implicit Arguments.
+Fixpoint size(t:tree) {struct t}: Z :=
+  match t with
+  | Empty => 0%Z
+  | (Node l _ r) => ((1%Z + (size l))%Z + (size r))%Z
+  end.
+Unset Implicit Arguments.
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem size_nonneg : forall (t:tree), (0%Z <= (size t))%Z.
+(* YOU MAY EDIT THE PROOF BELOW *)
+induction t; intuition.
+unfold size; fold size; omega.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/foveoos11_challenge2/why3session.xml

@@ -9,19 +9,11 @@
  <prover
   id="coq"
   name="Coq"
-  version="8.2pl1"/>
+  version="8.3pl2"/>
  <prover
   id="cvc3"
   name="CVC3"
   version="2.2"/>
- <prover
-  id="eprover"
-  name="Eprover"
-  version="0.7 Dhajea"/>
- <prover
-  id="gappa"
-  name="Gappa"
-  version="0.14.0"/>
  <prover
   id="simplify"
   name="Simplify"
@@ -29,11 +21,11 @@
  <prover
   id="yices"
   name="Yices"
-  version="1.0.13"/>
+  version="1.0.27"/>
  <prover
   id="z3"
   name="Z3"
-  version="2.13"/>
+  version="2.19"/>
  <file
   name="../foveoos11_challenge2.mlw"
   verified="true"
@@ -42,19 +34,33 @@
    name="WP MaximumTree"
    verified="true"
    expanded="true">
+   <goal
+    name="size_nonneg"
+    sum="d9dbfdf8e431c42e593667388fe56267"
+    proved="true"
+    expanded="true"
+    shape="ainfix >=asizeV0c0F">
+    <proof
+     prover="coq"
+     timelimit="10"
+     edited="foveoos11_challenge2_WP_MaximumTree_size_nonneg_1.v"
+     obsolete="false">
+     <result status="valid" time="0.46"/>
+    </proof>
+   </goal>
    <goal
     name="WP_parameter maximum"
     expl="parameter maximum"
-    sum="f40fb156943f0b6bc126f4aa41b513f4"
+    sum="633cd631bb850639d4b5effe2b5fcdf2"
     proved="true"
     expanded="true"
-    shape="CV0aEmptyfaNodeaEmptyVaEmptyainfix <=V2V1IamemV2V0FAamemV1V0aNodeVVaEmptyOaNodeaEmptyVVainfix <=V6amaxV5V3IamemV6V0FAamemamaxV5V3V0Iainfix <=V7V5IamemV7V4FAamemV5V4FAainfix =V4aEmptyNaNodeVVVainfix <=V13amaxV11amaxV9V12IamemV13V0FAamemamaxV11amaxV9V12V0Iainfix <=V14V12IamemV14V10FAamemV12V10FAainfix =V10aEmptyNIainfix <=V15V11IamemV15V8FAamemV11V8FAainfix =V8aEmptyNIainfix =V0aEmptyNF">
+    shape="CV0aEmptyfaNodeaEmptyVaEmptyainfix <=V2V1IamemV2V0FAamemV1V0aNodeVVaEmptyOaNodeaEmptyVVainfix <=V6amaxV5V3IamemV6V0FAamemamaxV5V3V0Iainfix <=V7V5IamemV7V4FAamemV5V4FAainfix =V4aEmptyNAainfix <asizeV4asizeV0Aainfix <=c0asizeV0aNodeVVVainfix <=V13amaxV11amaxV9V12IamemV13V0FAamemamaxV11amaxV9V12V0Iainfix <=V14V12IamemV14V10FAamemV12V10FAainfix =V10aEmptyNAainfix <asizeV10asizeV0Aainfix <=c0asizeV0Iainfix <=V15V11IamemV15V8FAamemV11V8FAainfix =V8aEmptyNAainfix <asizeV8asizeV0Aainfix <=c0asizeV0Iainfix =V0aEmptyNF">
     <proof
      prover="alt-ergo"
      timelimit="10"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.40"/>
+     <result status="valid" time="0.62"/>
     </proof>
    </goal>
   </theory>