diff options
Diffstat (limited to 'Test/vstte2012/Combinators.dfy')
| -rw-r--r-- | Test/vstte2012/Combinators.dfy | 459 |
1 files changed, 459 insertions, 0 deletions
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".)
+}
|