1 files changed, 26 insertions, 45 deletions

diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy
index 4a45d011..662024e4 100644
--- a/Test/vstte2012/Tree.dfy
+++ b/Test/vstte2012/Tree.dfy
@@ -22,9 +22,9 @@ datatype Result = Fail | Res(t: Tree, sOut: seq<int>)
 // The postconditions state properties that are needed

 // in the completeness proof.

 function toList(d: int, t: Tree): seq<int>

-  ensures toList(d, t) != [] && toList(d, t)[0] >= d;

-  ensures (toList(d, t)[0] == d) == (t == Leaf);

-  decreases t;

+  ensures toList(d, t) != [] && toList(d, t)[0] >= d

+  ensures (toList(d, t)[0] == d) == (t == Leaf)

+  decreases t

 {

   match t

   case Leaf => [d]

@@ -43,10 +43,10 @@ function toList(d: int, t: Tree): seq<int>
 function method build_rec(d: int, s: seq<int>): Result

   ensures build_rec(d, s).Res? ==>

             |build_rec(d, s).sOut| < |s| &&

-            build_rec(d, s).sOut == s[|s|-|build_rec(d, s).sOut|..];

+            build_rec(d, s).sOut == s[|s|-|build_rec(d, s).sOut|..]

   ensures build_rec(d, s).Res? ==>

-            toList(d,build_rec(d, s).t) == s[..|s|-|build_rec(d, s).sOut|];

-  decreases |s|, (if s==[] then 0 else s[0]-d);

+            toList(d,build_rec(d, s).t) == s[..|s|-|build_rec(d, s).sOut|]

+  decreases |s|, (if s==[] then 0 else s[0]-d)

 {

   if s==[] || s[0] < d then

     Fail

@@ -68,14 +68,14 @@ function method build_rec(d: int, s: seq<int>): Result
 // sequence yields exactly the input sequence.

 // Completeness is proved as a lemma, see below.

 function method build(s: seq<int>): Result

-  ensures build(s).Res? ==> toList(0,build(s).t) == s;

+  ensures build(s).Res? ==> toList(0,build(s).t) == s

 {

   var r := build_rec(0, s);

   if r.Res? && r.sOut == [] then r else Fail

 }

 

 

-// This ghost methods encodes the main lemma for the

+// This is the main lemma for the

 // completeness theorem. If a sequence s starts with a

 // valid encoding of a tree t then build_rec yields a

 // result (i.e., does not fail) and the rest of the sequence.

@@ -83,41 +83,39 @@ function method build(s: seq<int>): Result
 // induction on t. Dafny proves termination (using the

 // height of the term t as termination measure), which

 // ensures that the induction hypothesis is applied

-// correctly (encoded by calls to this ghost method).

-ghost method lemma0(t: Tree, d: int, s: seq<int>)

+// correctly (encoded by calls to this lemma).

+lemma lemma0(t: Tree, d: int, s: seq<int>)

   ensures build_rec(d, toList(d, t) + s).Res? &&

-          build_rec(d, toList(d, t) + s).sOut == s;

+          build_rec(d, toList(d, t) + s).sOut == s

 {

   match(t) {

   case Leaf =>

     assert toList(d, t) == [d];

   case Node(l, r) =>

     assert toList(d, t) + s == toList(d+1, l) + (toList(d+1, r) + s);

-

-    lemma0(l, d+1, toList(d+1, r) + s);  // apply the induction hypothesis

-    lemma0(r, d+1, s);  // apply the induction hypothesis

+    // the rest follows from (two invocations of) the (automatically applied) induction hypothesis

   }

 }

 

 

-// This ghost method encodes a lemma that states the

+// This lemma states the

 // completeness property. It is proved by applying the

 // main lemma (lemma0). In this lemma, the bound variables

 // of the completeness theorem are passed as arguments;

-// the following two ghost methods replace these arguments

+// the following two lemmas replace these arguments

 // by quantified variables.

-ghost method lemma1(t: Tree, s:seq<int>)

-  requires s == toList(0, t) + [];

-  ensures  build(s).Res?;

+lemma lemma1(t: Tree, s:seq<int>)

+  requires s == toList(0, t) + []

+  ensures build(s).Res?

 {

   lemma0(t, 0, []);

 }

 

 

-// This ghost method encodes a lemma that introduces the

-// existential quantifier in the completeness property.

-ghost method lemma2(s: seq<int>)

-  ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?;

+// This lemma introduces the existential quantifier in the completeness

+// property.

+lemma lemma2(s: seq<int>)

+  ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?

 {

   forall t | toList(0,t) == s {

     lemma1(t, s);

@@ -125,13 +123,13 @@ ghost method lemma2(s: seq<int>)
 }

 

 

-// This ghost method encodes the completeness theorem.

+// This lemma encodes the completeness theorem.

 // For each sequence for which there is a corresponding

 // tree, function build yields a result different from Fail.

 // The body of the method converts the argument of lemma2

 // into a universally quantified variable.

-ghost method completeness()

-  ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?);

+lemma completeness()

+  ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?)

 {

   forall s {

     lemma2(s);

@@ -145,21 +143,8 @@ ghost method completeness()
 // unfold the necessary definitions.

 method harness0()

   ensures build([1,3,3,2]).Res? &&

-          build([1,3,3,2]).t == Node(Leaf, Node(Node(Leaf, Leaf), Leaf));

+          build([1,3,3,2]).t == Node(Leaf, Node(Node(Leaf, Leaf), Leaf))

 {

-  assert build_rec(2, [2]) ==

-         Res(Leaf, []);

-  assert build_rec(2, [3,3,2]) ==

-         Res(Node(Leaf, Leaf), [2]);

-  assert build_rec(1, [3,3,2]) ==

-         Res(Node(Node(Leaf, Leaf), Leaf), []);

-  assert build_rec(1, [1,3,3,2]) ==

-         Res(Leaf, [3,3,2]);

-  assert build_rec(0, [1,3,3,2]) ==

-         Res(

-           Node(build_rec(1, [1,3,3,2]).t,

-                build_rec(1, [3,3,2]).t),

-           []);

 }

 

 

@@ -168,10 +153,6 @@ method harness0()
 // assertions are required by the verifier to

 // unfold the necessary definitions.

 method harness1()

-  ensures build([1,3,2,2]).Fail?;

+  ensures build([1,3,2,2]).Fail?

 {

-  assert build_rec(1,[1,3,2,2]) == Res(Leaf, [3,2,2]);

-  assert build_rec(3,[2,2]).Fail?;

-  assert build_rec(2,[3,2,2]).Fail?;

-  assert build_rec(1,[3,2,2]).Fail?;

 }