added a termination proof to example 'fill'

parent 87dd7bca
(* From Rustan Leino's tutorial on Dafny at VSTTE 2012
TODO: prove termination *)
(* From Rustan Leino's tutorial on Dafny at VSTTE 2012 *)
module Fill
......@@ -16,7 +14,17 @@ module Fill
| Node l y r -> contains l x || x = y || contains r x
end
let rec fill (t: tree) (a: array elt) (start: int) : int =
(* the size of a tree, to prove termination *)
function size (t: tree) : int = match t with
| Null -> 0
| Node l _ r -> size l + size r + 1
end
lemma size_nonneg: forall t: tree. size t >= 0
let rec fill (t: tree) (a: array elt) (start: int) : int
variant { size t }
=
{ 0 <= start <= length a }
match t with
| Null ->
......
(* 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.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| (mk_array _ elts1) => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| (mk_array length1 _) => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Parameter elt : Type.
Inductive tree :=
| Null : tree
| Node : tree -> elt -> tree -> tree .
Set Implicit Arguments.
Fixpoint contains(t:tree) (x:elt) {struct t}: Prop :=
match t with
| Null => False
| (Node l y r) => (contains l x) \/ ((x = y) \/ (contains r x))
end.
Unset Implicit Arguments.
Set Implicit Arguments.
Fixpoint size(t:tree) {struct t}: Z :=
match t with
| Null => 0%Z
| (Node l _ r) => (((size l) + (size r))%Z + 1%Z)%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; simpl; auto with *.
Qed.
(* DO NOT EDIT BELOW *)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="programs/fill/why3session.xml">
name="fill/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
name="Coq"
version="8.2pl2"/>
<file
name="../fill.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="WP Fill"
locfile="programs/fill/../fill.mlw"
locfile="fill/../fill.mlw"
loclnum="6" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="WP_parameter fill"
locfile="programs/fill/../fill.mlw"
loclnum="19" loccnumb="10" loccnume="14"
expl="parameter fill"
sum="0205a584fbde7e79af79a6195619dfa4"
name="size_nonneg"
locfile="fill/../fill.mlw"
loclnum="24" loccnumb="8" loccnume="19"
sum="8382205e1f534dc681a160909cc41727"
proved="true"
expanded="true"
shape="CV0aNullacontainsV0agetV3V4Iainfix <V4V2Aainfix <=V2V4FAainfix =agetV3V5agetV3V5Iainfix <V5V2Aainfix <=c0V5FAainfix <=V2V1Aainfix <=V2V2aNodeVVViainfix =V10V1NacontainsV0agetV12V14Iainfix <V14V13Aainfix <=V2V14FAainfix =agetV12V15agetV3V15Iainfix <V15V2Aainfix <=c0V15FAainfix <=V13V1Aainfix <=V2V13IacontainsV8agetV12V16Iainfix <V16V13Aainfix <=ainfix +V10c1V16FAainfix =agetV12V17agetV11V17Iainfix <V17ainfix +V10c1Aainfix <=c0V17FAainfix <=V13V1Aainfix <=ainfix +V10c1V13FFAainfix <=ainfix +V10c1V1Aainfix <=c0ainfix +V10c1Iainfix =V11asetV9V10V7FAainfix <V10V1Aainfix <=c0V10acontainsV0agetV9V18Iainfix <V18V10Aainfix <=V2V18FAainfix =agetV9V19agetV3V19Iainfix <V19V2Aainfix <=c0V19FAainfix <=V10V1Aainfix <=V2V10IacontainsV6agetV9V20Iainfix <V20V10Aainfix <=V2V20FAainfix =agetV9V21agetV3V21Iainfix <V21V2Aainfix <=c0V21FAainfix <=V10V1Aainfix <=V2V10FFAainfix <=V2V1Aainfix <=c0V2Iainfix <=V2V1Aainfix <=c0V2FFFF">
<label
name="expl:parameter fill">
</label>
shape="ainfix >=asizeV0c0F">
<proof
prover="1"
timelimit="10"
timelimit="15"
edited="fill_WP_Fill_size_nonneg_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.45"/>
</proof>
</goal>
<goal
name="WP_parameter fill"
locfile="fill/../fill.mlw"
loclnum="26" loccnumb="10" loccnume="14"
expl="parameter fill"
sum="2382af3dce215ccfb7a37bfd9f852d4a"
proved="true"
expanded="true"
shape="CV0aNullacontainsV0agetV3V4Iainfix <V4V2Aainfix <=V2V4FAainfix =agetV3V5agetV3V5Iainfix <V5V2Aainfix <=c0V5FAainfix <=V2V1Aainfix <=V2V2aNodeVVViainfix =V10V1NacontainsV0agetV12V14Iainfix <V14V13Aainfix <=V2V14FAainfix =agetV12V15agetV3V15Iainfix <V15V2Aainfix <=c0V15FAainfix <=V13V1Aainfix <=V2V13IacontainsV8agetV12V16Iainfix <V16V13Aainfix <=ainfix +V10c1V16FAainfix =agetV12V17agetV11V17Iainfix <V17ainfix +V10c1Aainfix <=c0V17FAainfix <=V13V1Aainfix <=ainfix +V10c1V13FFAainfix <=ainfix +V10c1V1Aainfix <=c0ainfix +V10c1Aainfix <asizeV8asizeV0Aainfix <=c0asizeV0Iainfix =V11asetV9V10V7FAainfix <V10V1Aainfix <=c0V10acontainsV0agetV9V18Iainfix <V18V10Aainfix <=V2V18FAainfix =agetV9V19agetV3V19Iainfix <V19V2Aainfix <=c0V19FAainfix <=V10V1Aainfix <=V2V10IacontainsV6agetV9V20Iainfix <V20V10Aainfix <=V2V20FAainfix =agetV9V21agetV3V21Iainfix <V21V2Aainfix <=c0V21FAainfix <=V10V1Aainfix <=V2V10FFAainfix <=V2V1Aainfix <=c0V2Aainfix <asizeV6asizeV0Aainfix <=c0asizeV0Iainfix <=V2V1Aainfix <=c0V2FFFF">
<label
name="expl:parameter fill">
</label>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="2"
timelimit="10"
timelimit="15"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.09"/>
</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