Merge

11 files changed, 278 insertions, 124 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index ce36e8c8..4ffccdc5 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -138,7 +138,7 @@ namespace Microsoft.Boogie {
     public bool Verify = true;

     public bool DisallowSoundnessCheating = false;

     public int DafnyInduction = 3;

-    public int DafnyInductionHeuristic = 3;

+    public int DafnyInductionHeuristic = 6;

     public bool TraceVerify = false;

     public int /*(0:3)*/ ErrorTrace = 1;

     public bool IntraproceduralInfer = true;

@@ -722,7 +722,7 @@ namespace Microsoft.Boogie {
 

           case "-inductionHeuristic":

           case "/inductionHeuristic":

-            ps.GetNumericArgument(ref DafnyInductionHeuristic, 4);

+            ps.GetNumericArgument(ref DafnyInductionHeuristic, 7);

             break;

 

           case "-contracts":

@@ -2052,9 +2052,10 @@ namespace Microsoft.Boogie {
                        heuristically chosen quantifiers and ghost methods

   /inductionHeuristic: 0 - least discriminating induction heuristic (that is,

                            lean toward applying induction more often)

-                       1 - more discriminating

-                       2 - even more discriminating

-                       3 (default) - most discriminating

+                       1,2,3,4,5 - levels in between, ordered as follows as

+                           far as how discriminating they are:

+                           0 < 1 < 2 < (3,4) < 5 < 6

+                       6 (default) - most discriminating

 

   ---- Boogie options --------------------------------------------------------

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a6198625..28146a7f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -6652,83 +6652,65 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// Returns 'true' iff

-    ///    there is a subexpression of 'expr' of the form 'F(...n...)' where 'F' is a recursive function

-    ///    and 'n' appears in an "elevated" subexpression of some decreases-contributing argument to 'F',

-    /// "elevated" essentially means "top-level or top-level under a + or -".

-    /// Variations, where a higher number means a more discriminating (and, consequently,

-    /// more complicated) heuristic:

-    ///   * DafnyInductionHeuristic==0:  always return 'true' no matter what

-    ///   * DafnyInductionHeuristic==1:  replace "elevated" by "any", and look at all arguments to 'F'

-    ///   * DafnyInductionHeuristic==2:  look at all arguments to 'F'

-    ///   * DafnyInductionHeuristic==3:  as stated above

+    /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'.

+    /// More precisely:

+    ///   DafnyInductionHeuristic      Return 'true'

+    ///   -----------------------      -------------

+    ///        0                       always

+    ///        1    if 'n' occurs as   any subexpression (of 'expr')

+    ///        2    if 'n' occurs as   any subexpression of          any index argument of an array/sequence select expression or any                       argument to a recursive function

+    ///        3    if 'n' occurs as   a prominent subexpression of  any index argument of an array/sequence select expression or any                       argument to a recursive function

+    ///        4    if 'n' occurs as   any subexpression of                                                                       any                       argument to a recursive function

+    ///        5    if 'n' occurs as   a prominent subexpression of                                                               any                       argument to a recursive function

+    ///        6    if 'n' occurs as   a prominent subexpression of                                                               any decreases-influencing argument to a recursive function

     /// Parameter 'n' is allowed to be a ThisSurrogate.

     /// </summary>

     bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {

       switch (CommandLineOptions.Clo.DafnyInductionHeuristic) {

         case 0: return true;

-        case 1: return VarOccursInArgumentToRecursiveFunction(expr, n, n);

-        default: return VarOccursInArgumentToRecursiveFunction(expr, n, null);

+        case 1: return ContainsFreeVariable(expr, false, n);

+        default: return VarOccursInArgumentToRecursiveFunction(expr, n, false);

       }

     }

 

     /// <summary>

-    /// Returns 'true' iff

-    ///    there is a subexpression of 'expr' of the form 'F(...n...)' where 'F' is a recursive function

-    ///    and 'n' appears in an "elevated" subexpression of some decreases-contributing argument to 'F',

-    ///    or

-    ///    'p' is non-null and 'p' appears in an "elevated" subexpression of 'expr'.

-    /// Variations:

-    ///   * DafnyInductionHeuristic LESS 2:  replace "elevated" by "any"

-    ///   * DafnyInductionHeuristic LESS 3:  look at all arguments to 'F'

-    /// Requires that 'p' is either 'null' of 'n'.

-    /// Parameters 'n' and 'p' are allowed to be a ThisSurrogate.

+    /// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or

+    /// not 'expr' prominent status in its context.

+    /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).

+    /// Parameter 'n' is allowed to be a ThisSurrogate.

     /// </summary>

-    bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, IVariable p) {

+    bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, bool exprIsProminent) {

       Contract.Requires(expr != null);

       Contract.Requires(n != null);

-      Contract.Requires(p == null || p == n);

 

-      var pForNotElevated = CommandLineOptions.Clo.DafnyInductionHeuristic < 2 ? p : null;

+      // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.

+      var subExprIsProminent = CommandLineOptions.Clo.DafnyInductionHeuristic == 2 || CommandLineOptions.Clo.DafnyInductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;

 

-      if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {

-        return false;

-      } else if (expr is ThisExpr) {

-        return p is ThisSurrogate;

+      if (expr is ThisExpr) {

+        return exprIsProminent && n is ThisSurrogate;

       } else if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

-        return p != null && e.Var == p;

-      } else if (expr is DisplayExpression) {

-        var e = (DisplayExpression)expr;

-        return e.Elements.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, pForNotElevated));  // subexpressions are not "elevated"

-      } else if (expr is FieldSelectExpr) {

-        var e = (FieldSelectExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.Obj, n, pForNotElevated);  // subexpressions are not "elevated"

+        return exprIsProminent && e.Var == n;

       } else if (expr is SeqSelectExpr) {

         var e = (SeqSelectExpr)expr;

-        var q = e.SelectOne ? pForNotElevated : p;

-        return VarOccursInArgumentToRecursiveFunction(e.Seq, n, pForNotElevated) ||  // this subexpression is not "elevated"

-          (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) ||  // this one is, if the SeqSelectExpr denotes a range

+        var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent;

+        return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) ||  // this subexpression does not acquire "prominent" status

+          (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) ||  // this one does (unless arrays/sequences are excluded)

           (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q));    // ditto

-      } else if (expr is SeqUpdateExpr) {

-        var e = (SeqUpdateExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.Seq, n, p) ||  // this subexpression is "elevated"

-          VarOccursInArgumentToRecursiveFunction(e.Index, n, pForNotElevated) ||  // but this one

-          VarOccursInArgumentToRecursiveFunction(e.Value, n, pForNotElevated);    // and this one are not

       } else if (expr is MultiSelectExpr) {

         var e = (MultiSelectExpr)expr;

-        // subexpressions are not "elevated"

-        return VarOccursInArgumentToRecursiveFunction(e.Array, n, pForNotElevated) ||

-          e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, pForNotElevated));

+        var q = CommandLineOptions.Clo.DafnyInductionHeuristic < 4 || subExprIsProminent;

+        return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) ||

+          e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));

       } else if (expr is FunctionCallExpr) {

         var e = (FunctionCallExpr)expr;

-        // For recursive functions:  arguments are "elevated"

-        // For non-recursive function:  arguments are "elevated" if the call is

+        // For recursive functions:  arguments are "prominent"

+        // For non-recursive function:  arguments are "prominent" if the call is

         var rec = e.Function.IsRecursive;

         bool inferredDecreases;  // we don't actually care

         var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases);

         bool variantArgument;

-        if (CommandLineOptions.Clo.DafnyInductionHeuristic < 3) {

+        if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) {

           variantArgument = rec;

         } else {

           // The receiver is considered to be "variant" if the function is recursive and the receiver participates

@@ -6736,26 +6718,14 @@ namespace Microsoft.Dafny {
           // of a term in the explicit decreases clause.

           variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, true, null));

         }

-        if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument ? n : p)) {

+        if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument || subExprIsProminent)) {

           return true;

         }

-#if DEBUG_TRACE

-        if (rec && !variantArgument) {

-          // rec is true, but variantArgument is not.  So, we passed in "p" whereas under the previous approach, we would have passed in "n".

-          if (n != p) {

-            // We can now say more precisely: we passed in "null", whereas the previous approach would have passed in "n"

-            if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, n)) {

-              // Moreover, passing in "null" instead of "n" actually made a difference here

-              Console.WriteLine("DEBUG: rec is true but variantArgument is not (this), and it made a difference");

-            }

-          }

-        }

-#endif

         Contract.Assert(e.Function.Formals.Count == e.Args.Count);

         for (int i = 0; i < e.Function.Formals.Count; i++) {

           var f = e.Function.Formals[i];

           var exp = e.Args[i];

-          if (CommandLineOptions.Clo.DafnyInductionHeuristic < 3) {

+          if (CommandLineOptions.Clo.DafnyInductionHeuristic < 6) {

             variantArgument = rec;

           } else {

             // The argument position is considered to be "variant" if the function is recursive and the argument participates

@@ -6763,46 +6733,25 @@ namespace Microsoft.Dafny {
             // of a term in the explicit decreases clause.

             variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, false, f));

           }

-          if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument ? n : p)) {

+          if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) {

             return true;

           }

-#if DEBUG_TRACE

-          if (rec && !variantArgument) {

-            // rec is true, but variantArgument is not.  So, we passed in "p" whereas under the previous approach, we would have passed in "n".

-            if (n != p) {

-              // We can now say more precisely: we passed in "null", whereas the previous approach would have passed in "n"

-              if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, n)) {

-                // Moreover, passing in "null" instead of "n" actually made a difference here

-                Console.WriteLine("DEBUG: rec is true but variantArgument is not ({0}), and it made a difference", f.Name);

-              }

-            }

-          }

-#endif

         }

         return false;

       } else if (expr is DatatypeValue) {

         var e = (DatatypeValue)expr;

-        var q = n.Type.IsDatatype ? p : pForNotElevated;

+        var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype

         return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));

       } else if (expr is OldExpr) {

         var e = (OldExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

-      } else if (expr is MultiSetFormingExpr) {

-        var e = (MultiSetFormingExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

-      } else if (expr is FreshExpr) {

-        var e = (FreshExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, pForNotElevated);

-      } else if (expr is AllocatedExpr) {

-        var e = (AllocatedExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, pForNotElevated);

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);  // prominent status continues

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

-        // arguments to both Not and SeqLength are "elevated"

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

+        // both Not and SeqLength preserve prominence

+        return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);

       } else if (expr is BinaryExpr) {

         var e = (BinaryExpr)expr;

-        IVariable q;

+        bool q;

         switch (e.ResolvedOp) {

           case BinaryExpr.ResolvedOpcode.Add:

           case BinaryExpr.ResolvedOpcode.Sub:

@@ -6813,36 +6762,39 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.Intersection:

           case BinaryExpr.ResolvedOpcode.SetDifference:

           case BinaryExpr.ResolvedOpcode.Concat:

-            // these operators have "elevated" arguments

-            q = p;

+            // these operators preserve prominence

+            q = exprIsProminent;

             break;

           default:

             // whereas all other binary operators do not

-            q = pForNotElevated;

+            q = subExprIsProminent;

             break;

         }

         return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||

           VarOccursInArgumentToRecursiveFunction(e.E1, n, q);

-      } else if (expr is ComprehensionExpr) {

-        var e = (ComprehensionExpr)expr;

-        return (e.Range != null && VarOccursInArgumentToRecursiveFunction(e.Range, n, pForNotElevated)) ||

-          VarOccursInArgumentToRecursiveFunction(e.Term, n, pForNotElevated);

       } else if (expr is ITEExpr) {

         var e = (ITEExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.Test, n, pForNotElevated) ||  // test is not "elevated"

-          VarOccursInArgumentToRecursiveFunction(e.Thn, n, p) ||                      // but the two branches are

-          VarOccursInArgumentToRecursiveFunction(e.Els, n, p);

-      } else if (expr is ConcreteSyntaxExpression) {

-        var e = (ConcreteSyntaxExpression)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.ResolvedExpression, n, p);

-      } else if (expr is BoxingCastExpr) {

-        var e = (BoxingCastExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

-      } else if (expr is UnboxingCastExpr) {

-        var e = (UnboxingCastExpr)expr;

-        return VarOccursInArgumentToRecursiveFunction(e.E, n, p);

+        return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) ||  // test is not "prominent"

+          VarOccursInArgumentToRecursiveFunction(e.Thn, n, exprIsProminent) ||  // but the two branches are

+          VarOccursInArgumentToRecursiveFunction(e.Els, n, exprIsProminent);

+      } else if (expr is OldExpr ||

+                 expr is ConcreteSyntaxExpression ||

+                 expr is BoxingCastExpr ||

+                 expr is UnboxingCastExpr) {

+        foreach (var exp in expr.SubExpressions) {

+          if (VarOccursInArgumentToRecursiveFunction(exp, n, exprIsProminent)) {  // maintain prominence

+            return true;

+          }

+        }

+        return false;

       } else {

-        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member

+        // in all other cases, reset the prominence status and recurse on the subexpressions

+        foreach (var exp in expr.SubExpressions) {

+          if (VarOccursInArgumentToRecursiveFunction(exp, n, subExprIsProminent)) {

+            return true;

+          }

+        }

+        return false;

       }

     }

 

@@ -6881,12 +6833,17 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Returns true iff 'v' occurs as a free variable in 'expr'.

+    /// Parameter 'v' is allowed to be a ThisSurrogate, in which case the method return true iff 'this'

+    /// occurs in 'expr'.

+    /// </summary>

     static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) {

       Contract.Requires(expr != null);

       Contract.Requires(lookForReceiver || v != null);

 

       if (expr is ThisExpr) {

-        return lookForReceiver;

+        return lookForReceiver || v is ThisSurrogate;

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

         return e.Var == v;

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index d53ae14b..ab10d944 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -88,8 +88,24 @@ Dafny program verifier finished with 33 verified, 0 errors
 Dafny program verifier finished with 141 verified, 0 errors

 

 -------------------- MoreInduction.dfy --------------------

-

-Dafny program verifier finished with 8 verified, 0 errors

+MoreInduction.dfy(75,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(74,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+MoreInduction.dfy(80,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(79,21): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+MoreInduction.dfy(85,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(84,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+MoreInduction.dfy(90,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(89,22): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 15 verified, 4 errors

 

 -------------------- Celebrity.dfy --------------------

 

diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index efba0963..84c32fb3 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -61,3 +61,37 @@ ghost method Lemma<X>(list: List<X>, ext: List<X>)
       }

   }

 }

+

+// ---------------------------------------------

+

+function NegFac(n: int): int

+  decreases -n;

+{

+  if -1 <= n then -1 else - NegFac(n+1) * n

+}

+

+ghost method LemmaAll()

+  ensures forall n :: NegFac(n) <= -1;  // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify

+{

+}

+

+ghost method LemmaOne(n: int)

+  ensures NegFac(n) <= -1;  // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify

+{

+}

+

+ghost method LemmaAll_Neg()

+  ensures forall n :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

+{

+}

+

+ghost method LemmaOne_Neg(n: int)

+  ensures NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

+{

+}

+

+ghost method LemmaOneWithDecreases(n: int)

+  ensures NegFac(n) <= -1;  // here, the programmer gives a good well-founded order, so this verifies

+  decreases -n;

+{

+}

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 4a1c4bbe..c9a9f3b7 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -397,9 +397,8 @@ ghost method P19()
 ghost method P20()

   ensures forall xs :: len(sort(xs)) == len(xs);

 {

-  // proving this theorem requires an additional lemma:

-  assert forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks));

-  // ...and one manually introduced case study:

+  P15();  // use the statement of problem 15 as a lemma

+  // ... and manually introduce a case distinction:

   assert forall ys ::

            sort(ys) == Nil ||

            exists z, zs :: sort(ys) == Cons(z, zs);

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index cc2e8acb..eed3eaa0 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -1,4 +1,8 @@
 

+-------------------- Classics.dfy --------------------

+

+Dafny program verifier finished with 5 verified, 0 errors

+

 -------------------- SnapshotableTrees.dfy --------------------

 

 Dafny program verifier finished with 36 verified, 0 errors

diff --git a/Test/dafny2/Classics.dfy b/Test/dafny2/Classics.dfy
new file mode 100644
index 00000000..68d9bf79
--- /dev/null
+++ b/Test/dafny2/Classics.dfy
@@ -0,0 +1,103 @@
+// A version of Turing's additive factorial program [Dr. A. Turing, "Checking a large routine",

+// In "Report of a Conference of High Speed Automatic Calculating Machines", pp. 67-69, 1949].

+

+function Factorial(n: nat): nat

+{

+  if n == 0 then 1 else n * Factorial(n-1)

+}

+

+method AdditiveFactorial(n: nat) returns (u: nat)

+  ensures u == Factorial(n);

+{

+  u := 1;

+  var r := 0;

+  while (r < n)

+    invariant 0 <= r <= n;

+    invariant u == Factorial(r);

+  {

+    var v := u;

+    var s := 1;

+    while (s <= r)

+      invariant 1 <= s <= r+1;

+      invariant u == s * Factorial(r);

+    {

+      u := u + v;

+      s := s + 1;

+    }

+    r := r + 1;

+  }

+}

+

+// Hoare's FIND program [C.A.R. Hoare, "Proof of a program: FIND", CACM 14(1): 39-45, 1971].

+// The proof annotations here are not the same as in Hoare's article.

+

+// In Hoare's words:

+//   This program operates on an array A[1:N], and a value of f (1 <= f <= N).

+//   Its effect is to rearrange the elements of A in such a way that:

+//     forall p,q (1 <= p <= f <= q <= N ==> A[p] <= A[f] <= A[q]).

+//

+// Here, we use 0-based indices, so we would say:

+//   This method operates on an array A[0..N], and a value of f (0 <= f < N).

+//   Its effect is to rearrange the elements of A in such a way that:

+//     forall p,q :: 0 <= p <= f <= q < N ==> A[p] <= A[f] <= A[q]).

+

+method FIND(A: array<int>, N: int, f: int)

+  requires A != null && A.Length == N;

+  requires 0 <= f < N;

+  modifies A;

+  ensures forall p,q :: 0 <= p <= f <= q < N ==> A[p] <= A[q];

+{

+  var m, n := 0, N-1;

+  while (m < n)

+    invariant 0 <= m <= f <= n < N;

+    invariant forall p,q :: 0 <= p < m <= q < N ==> A[p] <= A[q];

+    invariant forall p,q :: 0 <= p <= n < q < N ==> A[p] <= A[q];

+  {

+    var r, i, j := A[f], m, n;

+    while (i <= j)

+      invariant m <= i && j <= n;

+      invariant -1 <= j && i <= N;

+      invariant i <= j ==> exists g :: i <= g < N && r <= A[g];

+      invariant i <= j ==> exists g :: 0 <= g <= j && A[g] <= r;

+      invariant forall p :: 0 <= p < i ==> A[p] <= r;

+      invariant forall q :: j < q < N ==> r <= A[q];

+      // the following two invariants capture (and follow from) the fact that the array is not modified outside the [m:n] range

+      invariant forall p,q :: 0 <= p < m <= q < N ==> A[p] <= A[q];

+      invariant forall p,q :: 0 <= p <= n < q < N ==> A[p] <= A[q];

+      // the following invariant is used to prove progress of the outer loop

+      invariant (i==m && j==n && r==A[f]) || (m<i && j<n);

+    {

+      ghost var firstIteration := i==m && j==n;

+      while (A[i] < r)

+        invariant m <= i <= N && (firstIteration ==> i <= f);

+        invariant exists g :: i <= g < N && r <= A[g];

+        invariant exists g :: 0 <= g <= j && A[g] <= r;

+        invariant forall p :: 0 <= p < i ==> A[p] <= r;

+        decreases j - i;

+      { i := i + 1; }

+

+      while (r < A[j])

+        invariant 0 <= j <= n && (firstIteration ==> f <= j);

+        invariant exists g :: i <= g < N && r <= A[g];

+        invariant exists g :: 0 <= g <= j && A[g] <= r;

+        invariant forall q :: j < q < N ==> r <= A[q];

+        decreases j;

+      { j := j - 1; }

+

+      assert A[j] <= r <= A[i];

+      if (i <= j) {

+        var w := A[i]; A[i] := A[j]; A[j] := w;  // swap A[i] and A[j] (which may be referring to the same location)

+        assert A[i] <= r <= A[j];

+        i, j := i + 1, j - 1;

+      }

+    }

+

+    if (f <= j) {

+      n := j;

+    } else if (i <= f) {

+      m := i;

+    } else {

+      break;  // Hoare used a goto

+    }

+  }

+}

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index f6f25429..50b4ca18 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -5,7 +5,9 @@ set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

-for %%f in (SnapshotableTrees.dfy TreeBarrier.dfy

+for %%f in (

+    Classics.dfy

+    SnapshotableTrees.dfy TreeBarrier.dfy

     COST-verif-comp-2011-1-MaxArray.dfy

     COST-verif-comp-2011-2-MaxTree-class.dfy

     COST-verif-comp-2011-2-MaxTree-datatype.dfy

diff --git a/Test/textbook/Answer b/Test/textbook/Answer
index 50e96aca..dace3eb3 100644
--- a/Test/textbook/Answer
+++ b/Test/textbook/Answer
@@ -18,3 +18,7 @@ Boogie program verifier finished with 2 verified, 0 errors
 ------------------------------ McCarthy-91.bpl ---------------------

 

 Boogie program verifier finished with 1 verified, 0 errors

+

+------------------------------ TuringFactorial.bpl ---------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/textbook/TuringFactorial.bpl b/Test/textbook/TuringFactorial.bpl
new file mode 100644
index 00000000..37a3cb46
--- /dev/null
+++ b/Test/textbook/TuringFactorial.bpl
@@ -0,0 +1,33 @@
+// A Boogie version of Turing's additive factorial program, from "Checking a large routine"

+// published in the "Report of a Conference of High Speed Automatic Calculating Machines",

+// pp. 67-69, 1949.

+

+procedure ComputeFactorial(n: int) returns (u: int)

+  requires 1 <= n;

+  ensures u == Factorial(n);

+{

+  var r, v, s: int;

+  r, u := 1, 1;

+TOP:  // B

+  assert r <= n;

+  assert u == Factorial(r);

+  v := u;

+  if (n <= r) { return; }

+  s := 1;

+INNER:  // E

+  assert s <= r;

+  assert v == Factorial(r) && u == s * Factorial(r);

+  u := u + v;

+  s := s + 1;

+  assert s - 1 <= r;

+  if (s <= r) { goto INNER; }

+  r := r + 1;

+  goto TOP;

+}

+

+function Factorial(int): int;

+axiom Factorial(0) == 1;

+axiom (forall n: int :: {Factorial(n)}  1 <= n ==> Factorial(n) == n * Factorial_Aux(n-1));

+

+function Factorial_Aux(int): int;

+axiom (forall n: int :: {Factorial(n)} Factorial(n) == Factorial_Aux(n));

diff --git a/Test/textbook/runtest.bat b/Test/textbook/runtest.bat
index 265aa071..b747312d 100644
--- a/Test/textbook/runtest.bat
+++ b/Test/textbook/runtest.bat
@@ -6,7 +6,8 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe
 REM ======================

 REM ====================== Examples written in Boogie

 REM ======================

-for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl McCarthy-91.bpl) do (

+for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl McCarthy-91.bpl

+            TuringFactorial.bpl) do (

   echo.

   echo ------------------------------ %%f ---------------------

   %BPLEXE% %* %%f