diff options
Diffstat (limited to 'Test/vstte2012')
| -rw-r--r-- | Test/vstte2012/BreadthFirstSearch.dfy | 2 | ||||
| -rw-r--r-- | Test/vstte2012/Combinators.dfy | 12 | ||||
| -rw-r--r-- | Test/vstte2012/Tree.dfy | 71 |
3 files changed, 33 insertions, 52 deletions
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index b111a438..375f4a09 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class BreadthFirstSearch<Vertex(==)>
diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy index be7bc25f..ba4a4141 100644 --- a/Test/vstte2012/Combinators.dfy +++ b/Test/vstte2012/Combinators.dfy @@ -170,7 +170,7 @@ function IsTerminal(t: Term): bool // The following theorem states the correctness of the FindAndStep function:
-ghost method Theorem_FindAndStep(t: Term)
+lemma Theorem_FindAndStep(t: Term)
// If FindAndStep returns the term it started from, then there is no
// way to take a step. More precisely, there is no C[u] == t for which the
// Step applies to "u".
@@ -194,7 +194,7 @@ ghost method Theorem_FindAndStep(t: Term) // computes the value of FindAndStep(t) as it goes along and it returns
// that value.
-ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)
+lemma Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term)
ensures r == FindAndStep(t);
ensures r == t ==> IsTerminal(t);
ensures r != t ==>
@@ -255,7 +255,7 @@ ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term) // The proof of the lemma above used one more lemma, namely one that enumerates
// lays out the options for how to represent a term as a C[u] pair.
-ghost method Lemma_ContextPossibilities(t: Term)
+lemma Lemma_ContextPossibilities(t: Term)
ensures forall C,u :: IsContext(C) && t == EvalExpr(C, u) ==>
(C == Hole && t == u) ||
(t.Apply? && exists D :: C == C_term(D, t.cdr) && t.car == EvalExpr(D, u)) ||
@@ -442,7 +442,7 @@ function method ks(n: nat): Term // VerificationTask2) it computes the same thing as method VerificationTask2
// does.
-ghost method VerificationTask3()
+lemma VerificationTask3()
ensures forall n: nat ::
TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);
{
@@ -451,13 +451,13 @@ ghost method VerificationTask3() }
}
-ghost method VT3(n: nat)
+lemma VT3(n: nat)
ensures TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);
{
// Dafny's (way cool) induction tactic kicks in and proves the following
// assertion automatically:
assert forall p :: 2 <= p ==> FindAndStep(ks(p)) == ks(p-2);
- // And then Dafny's (cool beyond words) induction tactic for ghost methods kicks
+ // And then Dafny's (cool beyond words) induction tactic for lemmas kicks
// in to prove the postcondition. (If this got you curious, scope out Leino's
// VMCAI 2012 paper "Automating Induction with an SMT Solver".)
}
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?;
}
|