Added Dafny solutions to the VSTTE 2012 program verification competition

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".)

+}