diff options
| -rw-r--r-- | Test/alltests.txt | 1 | ||||
| -rw-r--r-- | Test/vstte2012/Answer | 20 | ||||
| -rw-r--r-- | Test/vstte2012/BreadthFirstSearch.dfy | 276 | ||||
| -rw-r--r-- | Test/vstte2012/Combinators.dfy | 459 | ||||
| -rw-r--r-- | Test/vstte2012/RingBuffer.dfy | 93 | ||||
| -rw-r--r-- | Test/vstte2012/Tree.dfy | 172 | ||||
| -rw-r--r-- | Test/vstte2012/Two-Way-Sort.dfy | 58 | ||||
| -rw-r--r-- | Test/vstte2012/runtest.bat | 24 |
8 files changed, 1103 insertions, 0 deletions
diff --git a/Test/alltests.txt b/Test/alltests.txt index e50d0a61..baffc2a1 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -27,6 +27,7 @@ dafny2 Use More Dafny examples havoc0 Use HAVOC-generated bpl files
VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
+vstte2012 Use Dafny solutions for the VSTTE 2012 program verification competition
livevars Use STORM benchmarks for testing correctness of live variable analysis
lazyinline Postponed Lazy inlining benchmarks
stratifiedinline Use Stratified inlining benchmarks
diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer new file mode 100644 index 00000000..15a95de1 --- /dev/null +++ b/Test/vstte2012/Answer @@ -0,0 +1,20 @@ +
+-------------------- Two-Way-Sort.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+
+-------------------- Combinators.dfy --------------------
+
+Dafny program verifier finished with 25 verified, 0 errors
+
+-------------------- RingBuffer.dfy --------------------
+
+Dafny program verifier finished with 13 verified, 0 errors
+
+-------------------- Tree.dfy --------------------
+
+Dafny program verifier finished with 15 verified, 0 errors
+
+-------------------- BreadthFirstSearch.dfy --------------------
+
+Dafny program verifier finished with 24 verified, 0 errors
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy new file mode 100644 index 00000000..5153b053 --- /dev/null +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -0,0 +1,276 @@ +class BreadthFirstSearch<Vertex>
+{
+ // The following function is left uninterpreted (for the purpose of the
+ // verification problem, it can be thought of as a parameter to the class)
+ function method Succ(x: Vertex): set<Vertex>
+
+ // This is the definition of what it means to be a path "p" from vertex
+ // "source" to vertex "dest"
+ function IsPath(source: Vertex, dest: Vertex, p: seq<Vertex>): bool
+ {
+ if source == dest then
+ p == []
+ else
+ p != [] && dest in Succ(p[|p|-1]) && IsPath(source, p[|p|-1], p[..|p|-1])
+ }
+
+ function IsClosed(S: set<Vertex>): bool // says that S is closed under Succ
+ {
+ forall v :: v in S ==> Succ(v) <= S
+ }
+
+ // This is the main method to be verified. Note, instead of using a
+ // postcondition that talks about that there exists a path (such that ...),
+ // this method returns, as a ghost out-parameter, that existential
+ // witness. The method could equally well have been written using an
+ // existential quantifier and no ghost out-parameter.
+ method BFS(source: Vertex, dest: Vertex, ghost AllVertices: set<Vertex>)
+ returns (d: int, ghost path: seq<Vertex>)
+ // source and dest are among AllVertices
+ requires source in AllVertices && dest in AllVertices;
+ // AllVertices is closed under Succ
+ requires IsClosed(AllVertices);
+ // This method has two basic outcomes, as indicated by the sign of "d".
+ // More precisely, "d" is non-negative iff "source" can reach "dest".
+ // The following postcondition says that under the "0 <= d" outcome,
+ // "path" denotes a path of length "d" from "source" to "dest":
+ ensures 0 <= d ==> IsPath(source, dest, path) && |path| == d;
+ // Moreover, that path is as short as any path from "source" to "dest":
+ ensures 0 <= d ==> forall p :: IsPath(source, dest, p) ==> |path| <= |p|;
+ // Finally, under the outcome "d < 0", there is no path from "source" to "dest":
+ ensures d < 0 ==> !exists p :: IsPath(source, dest, p);
+ {
+ var V, C, N := {source}, {source}, {};
+ ghost var Processed, paths := {}, Maplet({source}, source, [], Empty);
+ // V - all encountered vertices
+ // Processed - vertices reachable from "source" is at most "d" steps
+ // C - unprocessed vertices reachable from "source" in "d" steps
+ // (but no less)
+ // N - vertices encountered and reachable from "source" in "d+1" steps
+ // (but no less)
+ d := 0;
+ var dd := Zero;
+ while (C != {})
+ // V, Processed, C, N are all subsets of AllVertices:
+ invariant V <= AllVertices && Processed <= AllVertices && C <= AllVertices && N <= AllVertices;
+ // source is encountered:
+ invariant source in V;
+ // V is the disjoint union of Processed, C, and N:
+ invariant V == Processed + C + N;
+ invariant Processed !! C !! N; // Processed, C, and N are mutually disjoint
+ // "paths" records a path for every encountered vertex
+ invariant ValidMap(source, paths);
+ invariant V == Domain(paths);
+ // shortest paths for vertices in C have length d, and for vertices in N
+ // have length d+1
+ invariant forall x :: x in C ==> |Find(source, x, paths)| == d;
+ invariant forall x :: x in N ==> |Find(source, x, paths)| == d + 1;
+ // "dd" is just an inductive-looking way of writing "d":
+ invariant Value(dd) == d;
+ // "dest" is not reachable for any smaller value of "d":
+ invariant dest in R(source, dd, AllVertices) ==> dest in C;
+ invariant d != 0 ==> dest !in R(source, dd.predecessor, AllVertices);
+ // together, Processed and C are all the vertices reachable in at most d steps:
+ invariant Processed + C == R(source, dd, AllVertices);
+ // N are the successors of Processed that are not reachable within d steps:
+ invariant N == Successors(Processed, AllVertices) - R(source, dd, AllVertices);
+ // if we have exhausted C, then we have also exhausted N:
+ invariant C == {} ==> N == {};
+ // variant:
+ decreases AllVertices - Processed;
+ {
+ // remove a vertex "v" from "C"
+ var v := choose C;
+ C, Processed := C - {v}, Processed + {v};
+ ghost var pathToV := Find(source, v, paths);
+
+ if (v == dest) {
+ parallel (p | IsPath(source, dest, p))
+ ensures |pathToV| <= |p|;
+ {
+ Lemma_IsPath_R(source, dest, p, AllVertices);
+ if (|p| < |pathToV|) {
+ // show that this branch is impossible
+ ToNat_Value_Bijection(|p|);
+ RMonotonicity(source, ToNat(|p|), dd.predecessor, AllVertices);
+ }
+ }
+ return d, pathToV;
+ }
+
+ // process newly encountered successors
+ var newlyEncountered := set w | w in Succ(v) && w !in V;
+ V, N := V + newlyEncountered, N + newlyEncountered;
+ paths := UpdatePaths(newlyEncountered, source, paths, v, pathToV);
+
+ if (C == {}) {
+ C, N, d, dd := N, {}, d+1, Suc(dd);
+ }
+ }
+
+ // show that "dest" in not in any reachability set, no matter
+ // how many successors one follows
+ parallel (nn)
+ ensures dest !in R(source, nn, AllVertices);
+ {
+ if (Value(nn) < Value(dd)) {
+ RMonotonicity(source, nn, dd, AllVertices);
+ } else {
+ IsReachFixpoint(source, dd, nn, AllVertices);
+ }
+ }
+
+ // Now, show what what the above means in terms of IsPath. More
+ // precisely, show that there is no path "p" from "source" to "dest".
+ parallel (p | IsPath(source, dest, p))
+ // this and the previous two lines will establish the
+ // absurdity of a "p" satisfying IsPath(source, dest, p)
+ ensures false;
+ {
+ Lemma_IsPath_R(source, dest, p, AllVertices);
+ // a consequence of Lemma_IsPath_R is:
+ // dest in R(source, ToNat(|p|), AllVertices)
+ // but that contradicts the conclusion of the preceding parallel statement
+ }
+
+ d := -1; // indicate "no path"
+ }
+
+ // property of IsPath
+
+ ghost method Lemma_IsPath_Closure(source: Vertex, dest: Vertex,
+ p: seq<Vertex>, AllVertices: set<Vertex>)
+ requires IsPath(source, dest, p) && source in AllVertices && IsClosed(AllVertices);
+ ensures dest in AllVertices && forall v :: v in p ==> v in AllVertices;
+ {
+ if (p != []) {
+ var last := |p| - 1;
+ Lemma_IsPath_Closure(source, p[last], p[..last], AllVertices);
+ }
+ }
+
+ // operations on Nat
+
+ function Value(nn: Nat): nat
+ ensures ToNat(Value(nn)) == nn;
+ {
+ match nn
+ case Zero => 0
+ case Suc(mm) => Value(mm) + 1
+ }
+
+ function ToNat(n: nat): Nat
+ {
+ if n == 0 then Zero else Suc(ToNat(n - 1))
+ }
+
+ ghost method ToNat_Value_Bijection(n: nat)
+ ensures Value(ToNat(n)) == n;
+ {
+ // Dafny automatically figures out the inductive proof of the postcondition
+ }
+
+ // Reachability
+
+ function R(source: Vertex, nn: Nat, AllVertices: set<Vertex>): set<Vertex>
+ {
+ match nn
+ case Zero => {source}
+ case Suc(mm) => R(source, mm, AllVertices) +
+ Successors(R(source, mm, AllVertices), AllVertices)
+ }
+
+ function Successors(S: set<Vertex>, AllVertices: set<Vertex>): set<Vertex>
+ {
+ set w | w in AllVertices && exists x :: x in S && w in Succ(x)
+ }
+
+ ghost method RMonotonicity(source: Vertex, mm: Nat, nn: Nat, AllVertices: set<Vertex>)
+ requires Value(mm) <= Value(nn);
+ ensures R(source, mm, AllVertices) <= R(source, nn, AllVertices);
+ decreases Value(nn) - Value(mm);
+ {
+ if (Value(mm) < Value(nn)) {
+ RMonotonicity(source, Suc(mm), nn, AllVertices);
+ }
+ }
+
+ ghost method IsReachFixpoint(source: Vertex, mm: Nat, nn: Nat, AllVertices: set<Vertex>)
+ requires R(source, mm, AllVertices) == R(source, Suc(mm), AllVertices);
+ requires Value(mm) <= Value(nn);
+ ensures R(source, mm, AllVertices) == R(source, nn, AllVertices);
+ decreases Value(nn) - Value(mm);
+ {
+ if (Value(mm) < Value(nn)) {
+ IsReachFixpoint(source, Suc(mm), nn, AllVertices);
+ }
+ }
+
+ ghost method Lemma_IsPath_R(source: Vertex, x: Vertex,
+ p: seq<Vertex>, AllVertices: set<Vertex>)
+ requires IsPath(source, x, p) && source in AllVertices && IsClosed(AllVertices);
+ ensures x in R(source, ToNat(|p|), AllVertices);
+ {
+ if (p != []) {
+ Lemma_IsPath_Closure(source, x, p, AllVertices);
+ var last := |p| - 1;
+ Lemma_IsPath_R(source, p[last], p[..last], AllVertices);
+ }
+ }
+
+ // operations on Map's
+
+ function Domain(m: Map<Vertex>): set<Vertex>
+ {
+// if m.Maplet? then m.dom else {}
+// if m == Empty then {} else assert m.Maplet?; m.dom
+ match m
+ case Empty => {}
+ case Maplet(dom, t, s, nxt) => dom
+ }
+
+ // ValidMap encodes the consistency of maps (think, invariant).
+ // An explanation of this idiom is explained in the README file.
+ function ValidMap(source: Vertex, m: Map<Vertex>): bool
+ {
+ match m
+ case Empty => true
+ case Maplet(dom, v, path, next) =>
+ v in dom && dom == Domain(next) + {v} &&
+ IsPath(source, v, path) &&
+ ValidMap(source, next)
+ }
+
+ function Find(source: Vertex, x: Vertex, m: Map<Vertex>): seq<Vertex>
+ requires ValidMap(source, m) && x in Domain(m);
+ ensures IsPath(source, x, Find(source, x, m));
+ {
+ match m
+ case Maplet(dom, v, path, next) =>
+ if x == v then path else Find(source, x, next)
+ }
+
+ ghost method UpdatePaths(vSuccs: set<Vertex>, source: Vertex,
+ paths: Map<Vertex>, v: Vertex, pathToV: seq<Vertex>)
+ returns (newPaths: Map<Vertex>)
+ requires ValidMap(source, paths);
+ requires vSuccs !! Domain(paths);
+ requires forall succ :: succ in vSuccs ==> IsPath(source, succ, pathToV + [v]);
+ ensures ValidMap(source, newPaths) && Domain(newPaths) == Domain(paths) + vSuccs;
+ ensures forall x :: x in Domain(paths) ==>
+ Find(source, x, paths) == Find(source, x, newPaths);
+ ensures forall x :: x in vSuccs ==> Find(source, x, newPaths) == pathToV + [v];
+ {
+ if (vSuccs == {}) {
+ newPaths := paths;
+ } else {
+ var succ := choose vSuccs;
+ newPaths := Maplet(Domain(paths) + {succ}, succ, pathToV + [v], paths);
+ newPaths := UpdatePaths(vSuccs - {succ}, source, newPaths, v, pathToV);
+ }
+ }
+}
+
+datatype Map<T> = Empty | Maplet(dom: set<T>, T, seq<T>, next: Map<T>);
+
+datatype Nat = Zero | Suc(predecessor: Nat);
diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy new file mode 100644 index 00000000..46daf48d --- /dev/null +++ b/Test/vstte2012/Combinators.dfy @@ -0,0 +1,459 @@ +// Problem 2 concerns an interpreter for the language of S and K combinators.
+
+// -----------------------------------------------------------------------------
+// Definitions
+
+// First, we define the language of combinator terms. "Apply(x, y)" is what
+// the problem description writes as "(x y)". In the following Dafny
+// definition, "car" and "cdr" are declared to be destructors for terms
+// constructed by Apply.
+
+datatype Term = S | K | Apply(car: Term, cdr: Term);
+
+// The problem defines values to be a subset of the terms. More precisely,
+// a Value is a Term that fits the following grammar:
+// Value = K | S | (K Value) | (S Value) | ((S Value) Value)
+// The following predicate says whether or not a given term is a value.
+
+function method IsValue(t: Term): bool
+ ensures IsValue(t) && t.Apply? ==> IsValue(t.car) && IsValue(t.cdr);
+{
+ match t
+ case K => true
+ case S => true
+ case Apply(a, b) =>
+ match a
+ case K =>
+ assert IsValue(a);
+ IsValue(b)
+ case S =>
+ assert IsValue(a);
+ IsValue(b)
+ case Apply(x, y) =>
+ assert x==S && IsValue(y) && IsValue(b) ==> IsValue(a);
+ x==S && IsValue(y) && IsValue(b)
+}
+
+// A context is essentially a term with one missing subterm, a "hole". It
+// is defined as follows:
+
+datatype Context = Hole | C_term(Context, Term) | value_C(Term/*Value*/, Context);
+
+// The problem seems to suggest that the value_C form requires a value and
+// a context. To formalize that notion, we define a predicate that checks this
+// condition.
+
+function IsContext(C: Context): bool
+{
+ match C
+ case Hole => true // []
+ case C_term(D, t) => IsContext(D) // (D t)
+ case value_C(v, D) => IsValue(v) && IsContext(D) // (v D)
+}
+
+// The EvalExpr function replace the hole in a context with a given term.
+
+function EvalExpr(C: Context, t: Term): Term
+ requires IsContext(C);
+{
+ match C
+ case Hole => t
+ case C_term(D, u) => Apply(EvalExpr(D, t), u)
+ case value_C(v, D) => Apply(v, EvalExpr(D, t))
+}
+
+// A term can be reduced. This reduction operation is defined via
+// a single-step reduction operation. In the problem, the single-step
+// reduction has the form:
+// C[t] --> C[r]
+// We formalize the single-step reduction by a function Step, which
+// performs the reduction if it applies or just returns the given term
+// if it does. We will say that "Step applies" to refer to the first
+// case, which is a slight abuse of language, since the function "Step"
+// is total.
+//
+// Since the context C is the same on both sides in the single-step
+// reduction above, we don't pass it to function Step. Rather, Step
+// just takes a term "t" and returns the following:
+// match t
+// case ((K v1) v2) => v1
+// case (((S v1) v2) v3) => ((v1 v3) (v2 v3))
+// else t
+// As you can see below, it takes more lines than shown here to express
+// this matching in Dafny, but this is all that Step does.
+//
+// Again, note that Step returns the given term if neither or the two
+// vs in the problem statement applies.
+//
+// One more thing: Step has a postcondition (and the body of Step
+// contains three asserts that act as lemmas in proving the postcondition).
+// The postcondition has been included for the benefit of Verification
+// Task 2, and we describe the functions used in the Step postcondition
+// only much later in this file. For now, the postcondition can be
+// ignored, since it is, after all, just a consequence of the body
+// of Step.
+
+function method Step(t: Term): Term
+ ensures !ContainsS(t) ==>
+ !ContainsS(Step(t)) &&
+ (Step(t) == t || TermSize(Step(t)) < TermSize(t));
+{
+ match t
+ case S => t
+ case K => t
+ case Apply(x, y) =>
+ match x
+ case S => t
+ case K => t
+ case Apply(m, n) =>
+ if m == K && IsValue(n) && IsValue(y) then
+ // this is the case t == Apply(Apply(K, n), y)
+ assert !ContainsS(t) ==> !ContainsS(x);
+ assert TermSize(n) < TermSize(Apply(m, n));
+ n
+ else if m.Apply? && m.car == S && IsValue(m.cdr) && IsValue(n) && IsValue(y) then
+ // t == Apply(Apply(Apply(S, m.cdr), n), y)
+ assert ContainsS(m) && ContainsS(t);
+ Apply(Apply(m.cdr, y), Apply(n, y))
+ else
+ t
+}
+
+// The single-step reduction operation may be applied to any subexpression
+// of a term that could be considered a hole. Function FindAndStep
+// searches for a (context, term) pair C[u] that denotes a given term "t"
+// such that Step applies to "u". If found, the function returns
+// C[Step(u)], which will necessarily be different from "t". If no such
+// C[u] pair exists, this function returns the given "t".
+//
+// Note, FindAndStep only applies one Step. We will get to repeated
+// applications of steps in the "reduction" method below.
+//
+// For all definitions above, it was necessary to check (manually) that
+// they correspond to the definitions intended in the problem statement.
+// That is, the definitions above are all part of the specification.
+// For function FindAndStep, the definition given does not require
+// such scrutiny. Rather, we will soon state a theorem that states
+// the properties of what FindAndStep returns.
+//
+// Like Step, FindAndStep has a postcondition, and it is also included to
+// support Verification Task 2.
+
+function method FindAndStep(t: Term): Term
+ ensures !ContainsS(t) ==>
+ !ContainsS(FindAndStep(t)) &&
+ (FindAndStep(t) == t || TermSize(FindAndStep(t)) < TermSize(t));
+{
+ if Step(t) != t then
+ Step(t)
+ else if !t.Apply? then
+ t
+ else if FindAndStep(t.car) != t.car then
+ Apply(FindAndStep(t.car), t.cdr)
+ else if IsValue(t.car) && FindAndStep(t.cdr) != t.cdr then
+ Apply(t.car, FindAndStep(t.cdr))
+ else
+ t
+}
+
+// One part of the correctness of FindAndStep (and, indeed, of method
+// "reduction" below) is that a term can be terminal, meaning that there is
+// no way to apply Step to any part of it.
+
+function IsTerminal(t: Term): bool
+{
+ !(exists C,u :: IsContext(C) && t == EvalExpr(C,u) && Step(u) != u)
+}
+
+// The following theorem states the correctness of the FindAndStep function:
+
+ghost method 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".
+ ensures FindAndStep(t) == t ==> IsTerminal(t);
+ // If FindAndStep returns a term that's different from what it started with,
+ // then it chose some C[u] == t for which the Step applies to "u", and then
+ // it returned C[Step(u)].
+ ensures FindAndStep(t) != t ==>
+ exists C,u :: IsContext(C) && t == EvalExpr(C,u) && Step(u) != u &&
+ FindAndStep(t) == EvalExpr(C, Step(u));
+{
+ // The theorem follows from the following lemma, which itself is proved by
+ // induction.
+ var r, C, u := Lemma_FindAndStep(t);
+}
+
+// This is the lemma that proves the theorem above. Whereas the theorem talks
+// existentially about C and u, the lemma constructs C and u and returns them,
+// which is useful in the proof by induction. The computation inside the
+// lemma mimicks that done by function FindAndStep; indeed, the lemma
+// 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)
+ ensures r == FindAndStep(t);
+ ensures r == t ==> IsTerminal(t);
+ ensures r != t ==>
+ IsContext(C) && t == EvalExpr(C,u) && Step(u) != u &&
+ r == EvalExpr(C, Step(u));
+{
+ Lemma_ContextPossibilities(t);
+ if (Step(t) != t) {
+ // t == Hole[t] and Step applies t. So, return Hole[Step(t)]
+ return Step(t), Hole, t;
+ } else if (!t.Apply?) {
+ r := t;
+ } else {
+ r, C, u := Lemma_FindAndStep(t.car); // (*)
+ if (r != t.car) {
+ // t has the form (a b) where a==t.car and b==t.cdr, and a==C[u] for some
+ // context C and some u to which the Step applies. t can therefore be
+ // denoted by (C[u] b) == (C b)[u] and the Step applies to u. So, return
+ // (C b)[Step(u)] == (C[Step(u)] b). Note that FindAndStep(a)
+ // gives C[Step(u)].
+ return Apply(r, t.cdr), C_term(C, t.cdr), u;
+ } else if (IsValue(t.car)) {
+ r, C, u := Lemma_FindAndStep(t.cdr);
+ assert IsTerminal(t.car); // make sure this is still remembered from (*)
+
+ if (r != t.cdr) {
+ // t has the form (a b) where a==t.car and b==t.cdr and "a" is a Value,
+ // and b==C[u] for some context C and some u to which the Step applies.
+ // t can therefore be denoted by (a C[u]) == (C a)[u] and the Step
+ // applies to u. So, return (C a)[Step(u)] == (a C[Step(u)]). Note
+ // that FindAndStep(b) gives C[Step(u)].
+ return Apply(t.car, r), value_C(t.car, C), u;
+ } else {
+ parallel (C,u | IsContext(C) && t == EvalExpr(C,u))
+ ensures Step(u) == u;
+ {
+ // The following assert and the first assert of each "case" are
+ // consequences of the Lemma_ContextPossibilities that was invoked
+ // above.
+ assert t.Apply? && IsValue(t.car);
+ match (C) {
+ case Hole =>
+ assert t == u;
+ case C_term(D, bt) =>
+ assert bt == t.cdr && t.car == EvalExpr(D, u);
+ case value_C(at, D) =>
+ assert at == t.car && t.cdr == EvalExpr(D, u);
+ }
+ }
+ r := t;
+ }
+ } else {
+ r := t;
+ }
+ }
+}
+
+// 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)
+ 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)) ||
+ (t.Apply? && IsValue(t.car) &&
+ exists D :: C == value_C(t.car, D) && t.cdr == EvalExpr(D, u));
+{
+ // Dafny's induction tactic rocks
+}
+
+// We now define a way to record a sequence of reduction steps.
+// IsTrace(trace, t, r) returns true iff "trace" gives witness to a
+// sequence of terms from "t" to "r", each term reducing to its
+// successor in the trace.
+
+datatype Trace = EmptyTrace | ReductionStep(Trace, Term);
+
+function IsTrace(trace: Trace, t: Term, r: Term): bool
+{
+ match trace
+ case EmptyTrace =>
+ t == r
+ case ReductionStep(tr, u) =>
+ IsTrace(tr, t, u) && FindAndStep(u) == r
+}
+
+// Finally, we are ready to give the requested routine "reduction", which
+// keeps applying FindAndStep until quiescence, that is, until Step
+// no longer applies.
+//
+// As required by Verification Task 1, the "reduction" method has two
+// postconditions. One says that the term returned, "r", was obtained
+// from the original term, "t", by a sequence of reduction steps. The
+// other says that "r" cannot be reduced any further.
+//
+// Unlike the other competition problems, this one requested code
+// (for "reduction") that may not terminate. In order to allow reasoning
+// about algorithms that may never terminate, Dafny has a special loop
+// statement (a "while" loop with a declaration "decreases *") that
+// thus comes in handy for "reduction". (Dafny never allows recursion
+// to be non-terminating, only these special loops.) Note that use
+// of the special loop statement does not have any effect on the
+// specifications of the enclosing method (but this may change in a
+// future version of Dafny).
+
+method reduction(t: Term) returns (r: Term)
+ // The result was obtained by a sequence of reductions:
+ ensures exists trace :: IsTrace(trace, t, r);
+ // The result "r" cannot be reduced any further:
+ ensures IsTerminal(r);
+{
+ r := t;
+ ghost var trace := EmptyTrace;
+ while (true)
+ invariant IsTrace(trace, t, r);
+ decreases *; // allow this statement to loop forever
+ {
+ var u := FindAndStep(r);
+ if (u == r) {
+ // we have found a fixpoint
+ Theorem_FindAndStep(r);
+ return;
+ }
+ r, trace := u, ReductionStep(trace, r);
+ }
+}
+
+// -----------------------------------------------------------------------------
+// Verification Task 2
+//
+// This part of the problem asks us to consider the reduction of terms that
+// do not contain S. The following function formalizes what it means for a term
+// to contain S:
+
+function method ContainsS(t: Term): bool
+{
+ match t
+ case S => true
+ case K => false
+ case Apply(x, y) => ContainsS(x) || ContainsS(y)
+}
+
+// The verification task itself is to prove that "reduction" terminates on any
+// term that does not contain S. To prove this, we need to supply a loop variant
+// for the loop in "reduction". However, Dafny does not allow one loop to be
+// proved to terminate in some cases and allowed not to terminate in other cases.
+// There, we meet Verification Task 2 by manually copying the body of "reduction"
+// into a new method (called VerificationTask2) and proving that this new method
+// terminates. Of course, Dafny does not check that we copy the body correctly,
+// so that needs to be checked by a human.
+//
+// In method VerificationTask2, we added not just the precondition given in the
+// Verification Task and a loop variant, but we also added two loop invariants
+// and one more postcondition. One of the loop invariants keep track of that
+// there are no S's. The other loop invariant and the postcondition are for
+// the benefit of Verification Task 3, as we explain later.
+
+method VerificationTask2(t: Term) returns (r: Term)
+ requires !ContainsS(t); // a sufficient condition for termination
+ // The result was obtained by a sequence of reductions:
+ ensures exists trace :: IsTrace(trace, t, r);
+ // The result "r" cannot be reduced any further:
+ ensures IsTerminal(r);
+ // Later in this file, we define a function TerminatingReduction, and the
+ // following postcondition says that TerminatingReduction computes the same
+ // term as this method does.
+ ensures r == TerminatingReduction(t);
+{
+ r := t;
+ ghost var trace := EmptyTrace;
+ while (true)
+ invariant IsTrace(trace, t, r) && !ContainsS(r);
+ invariant TerminatingReduction(t) == TerminatingReduction(r);
+ decreases TermSize(r);
+ {
+ var u := FindAndStep(r);
+ if (u == r) {
+ // we have found a fixpoint
+ Theorem_FindAndStep(r);
+ return;
+ }
+ r, trace := u, ReductionStep(trace, r);
+ }
+}
+
+// What now follows is the definition TermSize, which is used in the
+// loop variant. When a Step is applied to a term without S, TermSize
+// is reduced, which is stated as a postcondition of both Step and
+// FindAndStep. That postcondition of FindAndStep is used in the
+// proof of termination of method VerificationTask2.
+
+// The loop variant is simply the count of nodes in the term:
+
+function TermSize(t: Term): nat
+{
+ match t
+ case S => 1
+ case K => 1
+ case Apply(x, y) => 1 + TermSize(x) + TermSize(y)
+}
+
+// We have already given two methods for computing a reduction:
+// method "reduction", which may or may not terminate, and method
+// "VerificationTask2", whose precondition is strong enough to let
+// us prove that the method will terminate. The correspondence
+// between the two methods is checked by hand, seeing that
+// VerificationTask2 includes the postconditions of "reduction" and
+// seeing that the code is the same.
+//
+// We now define a third way of computing reductions, this time
+// using a function (not a method). To prove that this function
+// computes the same thing as method VerificationTask2, we had
+// added a postcondition to VerificationTask2 above. This function
+// is introduced for the benefit of stating and verifying Verification
+// Task 3.
+
+function TerminatingReduction(t: Term): Term
+ requires !ContainsS(t); // a sufficient condition for termination
+ decreases TermSize(t);
+{
+ if FindAndStep(t) == t then
+ t // we have reached a fixpoint
+ else
+ TerminatingReduction(FindAndStep(t))
+}
+
+// -----------------------------------------------------------------------------
+// Verification Task 3
+
+// Here is the function "ks" from Verification Task 3. It produces a particular
+// family of terms that contain only Apply and K. Hence, we can establish, as a
+// postcondition of the function, that ks(n) does not contain S.
+
+function method ks(n: nat): Term
+ ensures !ContainsS(ks(n));
+{
+ if n == 0 then K else Apply(ks(n-1), K)
+}
+
+// Verification Task 3 is now established by the following theorem. It says
+// that reducing ks(n) results in either K and (K K), depending on the parity
+// of n. The theorem uses function TerminatingReduction to speak of the
+// reduction--remember that (by the last postcondition of method
+// VerificationTask2) it computes the same thing as method VerificationTask2
+// does.
+
+ghost method VerificationTask3()
+ ensures forall n: nat ::
+ TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);
+{
+ parallel (n: nat) {
+ VT3(n);
+ }
+}
+
+ghost method 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
+ // 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/RingBuffer.dfy b/Test/vstte2012/RingBuffer.dfy new file mode 100644 index 00000000..5262e462 --- /dev/null +++ b/Test/vstte2012/RingBuffer.dfy @@ -0,0 +1,93 @@ +class RingBuffer<T>
+{
+ // public fields that are used to define the abstraction:
+ ghost var Contents: seq<T>; // the contents of the ring buffer
+ ghost var N: nat; // the capacity of the ring buffer
+ ghost var Repr: set<object>; // the set of objects used in the implementation
+
+ // Valid encodes the consistency of RingBuffer objects (think, invariant).
+ // An explanation of this idiom is explained in the README file.
+ function Valid(): bool
+ reads this, Repr;
+ {
+ this in Repr && null !in Repr &&
+ data != null && data in Repr &&
+ data.Length == N &&
+ (N == 0 ==> len == first == 0 && Contents == []) &&
+ (N != 0 ==> len <= N && first < N) &&
+ Contents == if first + len <= N then data[first..first+len]
+ else data[first..] + data[..first+len-N]
+ }
+
+ // private implementation:
+ var data: array<T>;
+ var first: nat;
+ var len: nat;
+
+ constructor Create(n: nat)
+ modifies this;
+ ensures Valid() && fresh(Repr - {this});
+ ensures Contents == [] && N == n;
+ {
+ Repr := {this};
+ data := new T[n];
+ Repr := Repr + {data};
+ first, len := 0, 0;
+ Contents, N := [], n;
+ }
+
+ method Clear()
+ requires Valid();
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures Contents == [] && N == old(N);
+ {
+ len := 0;
+ Contents := [];
+ }
+
+ method Head() returns (x: T)
+ requires Valid();
+ requires Contents != [];
+ ensures x == Contents[0];
+ {
+ x := data[first];
+ }
+
+ method Push(x: T)
+ requires Valid();
+ requires |Contents| != N;
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures Contents == old(Contents) + [x] && N == old(N);
+ {
+ var nextEmpty := if first + len < data.Length
+ then first + len else first + len - data.Length;
+ data[nextEmpty] := x;
+ len := len + 1;
+ Contents := Contents + [x];
+ }
+
+ method Pop() returns (x: T)
+ requires Valid();
+ requires Contents != [];
+ modifies Repr;
+ ensures Valid() && fresh(Repr - old(Repr));
+ ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);
+ {
+ x := data[first];
+ first, len := if first + 1 == data.Length then 0 else first + 1, len - 1;
+ Contents := Contents[1..];
+ }
+}
+
+method TestHarness(x: int, y: int, z: int)
+{
+ var b := new RingBuffer<int>.Create(2);
+ b.Push(x);
+ b.Push(y);
+ var h := b.Pop(); assert h == x;
+ b.Push(z);
+ h := b.Pop(); assert h == y;
+ h := b.Pop(); assert h == z;
+}
diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy new file mode 100644 index 00000000..47ed19a4 --- /dev/null +++ b/Test/vstte2012/Tree.dfy @@ -0,0 +1,172 @@ +// The tree datatype
+datatype Tree = Leaf | Node(Tree, Tree);
+
+
+// This datatype is used for the result of the build functions.
+// These functions either fail or yield a tree. Since we use
+// a side-effect free implementation of the helper
+// build_rec, it also has to yield the rest of the sequence,
+// which still needs to be processed. For function build,
+// this part is not used.
+datatype Result = Fail | Res(t: Tree, sOut: seq<int>);
+
+
+// Function toList converts a tree to a sequence.
+// We use Dafny's built-in value type sequence rather than
+// an imperative implementation to simplify verification.
+// The argument d is added to each element of the sequence;
+// it is analogous to the argument d in build_rec.
+// 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;
+{
+ match t
+ case Leaf => [d]
+ case Node(l, r) => toList(d+1, l) + toList(d+1, r)
+}
+
+
+// Function build_rec is a side-effect free implementation
+// of the code given in the problem statement.
+// The first postcondition is needed to show that the
+// termination measure indeed decreases.
+// The second postcondition specifies the soundness
+// property; converting the resulting tree back into a
+// sequence yields exactly that portion of the input
+// sequence that has been consumed.
+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|..];
+ 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);
+{
+ if s==[] || s[0] < d then
+ Fail
+ else if s[0] == d then
+ Res(Leaf, s[1..])
+ else
+ var left := build_rec(d+1, s);
+ if left.Fail? then Fail else
+ var right := build_rec(d+1, left.sOut);
+ if right.Fail? then Fail else
+ Res(Node(left.t, right.t), right.sOut)
+}
+
+
+// Function build is a side-effect free implementation
+// of the code given in the problem statement.
+// The postcondition specifies the soundness property;
+// converting the resulting tree back into a
+// 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;
+{
+ var r := build_rec(0, s);
+ if r.Res? && r.sOut == [] then r else Fail
+}
+
+
+// This ghost methods encodes 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.
+// The body of the method proves the lemma by structural
+// 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>)
+ ensures build_rec(d, toList(d, t) + s).Res? &&
+ 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
+ }
+}
+
+
+// This ghost method encodes a lemma that 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
+// by quantified variables.
+ghost method 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?;
+{
+ parallel(t | toList(0,t) == s) {
+ lemma1(t, s);
+ }
+}
+
+
+// This ghost method 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?);
+{
+ parallel(s) {
+ lemma2(s);
+ }
+}
+
+
+// This method encodes the first test harness
+// given in the problem statement. The local
+// assertions are required by the verifier to
+// 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));
+{
+ 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),
+ []);
+}
+
+
+// This method encodes the second test harness
+// given in the problem statement. The local
+// assertions are required by the verifier to
+// unfold the necessary definitions.
+method harness1()
+ ensures build([1,3,2,2]).Fail?;
+{
+ assert build_rec(3, [2,2]).Fail?;
+ assert build_rec(1, [3,2,2]).Fail?;
+}
diff --git a/Test/vstte2012/Two-Way-Sort.dfy b/Test/vstte2012/Two-Way-Sort.dfy new file mode 100644 index 00000000..49ff29b4 --- /dev/null +++ b/Test/vstte2012/Two-Way-Sort.dfy @@ -0,0 +1,58 @@ +// This method is a slight generalization of the
+// code provided in the problem statement since it
+// is generic in the type of the array elements.
+method swap<T>(a: array<T>, i: int, j: int)
+ requires a != null;
+ requires 0 <= i < j < a.Length;
+ modifies a;
+ ensures a[i] == old(a[j]);
+ ensures a[j] == old(a[i]);
+ ensures forall m :: 0 <= m < a.Length && m != i && m != j ==> a[m] == old(a[m]);
+ ensures multiset(a[..]) == old(multiset(a[..]));
+{
+ var t := a[i];
+ a[i] := a[j];
+ a[j] := t;
+}
+
+// This method is a direct translation of the pseudo
+// code given in the problem statement.
+// The first postcondition expresses that the resulting
+// array is sorted, that is, all occurrences of "false"
+// come before all occurrences of "true".
+// The second postcondition expresses that the post-state
+// array is a permutation of the pre-state array. To express
+// this, we use Dafny's built-in multisets. The built-in
+// function "multiset" takes an array and yields the
+// multiset of the array elements.
+// Note that Dafny guesses a suitable ranking function
+// for the termination proof of the while loop.
+// We use the loop guard from the given pseudo-code. However,
+// the program also verifies with the stronger guard "i < j"
+// (without changing any of the other specifications or
+// annotations).
+method two_way_sort(a: array<bool>)
+ requires a != null;
+ modifies a;
+ ensures forall m,n :: 0 <= m < n < a.Length ==> (!a[m] || a[n]);
+ ensures multiset(a[..]) == old(multiset(a[..]));
+{
+ var i := 0;
+ var j := a.Length - 1;
+ while (i <= j)
+ invariant 0 <= i <= j + 1 <= a.Length;
+ invariant forall m :: 0 <= m < i ==> !a[m];
+ invariant forall n :: j < n < a.Length ==> a[n];
+ invariant multiset(a[..]) == old(multiset(a[..]));
+ {
+ if (!a[i]) {
+ i := i+1;
+ } else if (a[j]) {
+ j := j-1;
+ } else {
+ swap(a, i, j);
+ i := i+1;
+ j := j-1;
+ }
+ }
+}
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat new file mode 100644 index 00000000..07b5859e --- /dev/null +++ b/Test/vstte2012/runtest.bat @@ -0,0 +1,24 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
+
+for %%f in (
+ Two-Way-Sort.dfy
+ Combinators.dfy
+ RingBuffer.dfy
+ Tree.dfy
+ BreadthFirstSearch.dfy
+ ) do (
+ echo.
+ echo -------------------- %%f --------------------
+
+ REM The following line will just run the verifier
+ IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
+
+ REM Alternatively, the following lines also produce C# code and compile it
+ IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
+ IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
+)
|