Dafny: compile quantifiers

Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction
Dafny: split expressions when proving function postconditions
Boogie and BVD: updated copyright year ranges

11 files changed, 771 insertions, 84 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index dc7caac7..decc5223 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -102,7 +102,7 @@ namespace Microsoft.Dafny {
     void CompileBuiltIns(BuiltIns builtIns) {

       wr.WriteLine("namespace Dafny {");

       Indent(IndentAmount);

-      wr.WriteLine("public class Helpers {");

+      wr.WriteLine("public partial class Helpers {");

       foreach (var decl in builtIns.SystemModule.TopLevelDecls) {

         if (decl is ArrayClassDecl) {

           int dims = ((ArrayClassDecl)decl).Dims;

@@ -1262,7 +1262,43 @@ namespace Microsoft.Dafny {
         }

       

       } else if (expr is QuantifierExpr) {

-        Contract.Assert(false); throw new cce.UnreachableException();  // a quantifier is always a ghost

+        var e = (QuantifierExpr)expr;

+        Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds

+        var n = e.BoundVars.Count;

+        Contract.Assert(e.Bounds.Count == n);

+        for (int i = n; 0 <= --i; ) {

+          var bound = e.Bounds[i];

+          var bv = e.BoundVars[i];

+          // emit:  Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)

+          if (bound is QuantifierExpr.BoolBoundedPool) {

+            wr.Write("Dafny.Helpers.QuantBool(");

+          } else if (bound is QuantifierExpr.IntBoundedPool) {

+            var b = (QuantifierExpr.IntBoundedPool)bound;

+            wr.Write("Dafny.Helpers.QuantInt(");

+            TrExpr(b.LowerBound);

+            wr.Write(", ");

+            TrExpr(b.UpperBound);

+            wr.Write(", ");

+          } else if (bound is QuantifierExpr.SetBoundedPool) {

+            var b = (QuantifierExpr.SetBoundedPool)bound;

+            wr.Write("Dafny.Helpers.QuantSet(");

+            TrExpr(b.Set);

+            wr.Write(", ");

+          } else if (bound is QuantifierExpr.SeqBoundedPool) {

+            var b = (QuantifierExpr.SeqBoundedPool)bound;

+            wr.Write("Dafny.Helpers.QuantSeq(");

+            TrExpr(b.Seq);

+            wr.Write(", ");

+          } else {

+            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

+          }

+          wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

+          wr.Write("{0} => ", bv.Name);

+        }

+        TrExpr(e.Body);

+        for (int i = 0; i < n; i++) {

+          wr.Write(")");

+        }

       

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index a8acb013..b26e1288 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1732,6 +1732,10 @@ namespace Microsoft.Dafny {
 

       this.tok = tok;

     }

+

+    public virtual IEnumerable<Expression> SubExpressions {

+      get { yield break; }

+    }

   }

 

   public class LiteralExpr : Expression {

@@ -1802,7 +1806,10 @@ namespace Microsoft.Dafny {
       this.DatatypeName = datatypeName;

       this.MemberName = memberName;

       this.Arguments = arguments;

+    }

 

+    public override IEnumerable<Expression> SubExpressions {

+      get { return Arguments; }

     }

   }

 

@@ -1835,8 +1842,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Name = name;

-

-

     }

   }

 

@@ -1851,7 +1856,10 @@ namespace Microsoft.Dafny {
       : base(tok) {

       Contract.Requires(cce.NonNullElements(elements));

       Elements = elements;

+    }

 

+    public override IEnumerable<Expression> SubExpressions {

+      get { return Elements; }

     }

   }

 

@@ -1882,7 +1890,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(FieldName != null);

     }

 

-

     public FieldSelectExpr(IToken tok, Expression obj, string fieldName)

       : base(tok) {

       Contract.Requires(tok != null);

@@ -1890,7 +1897,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(fieldName != null);

       this.Obj = obj;

       this.FieldName = fieldName;

+    }

 

+    public override IEnumerable<Expression> SubExpressions {

+      get { yield return Obj; }

     }

   }

 

@@ -1918,6 +1928,14 @@ namespace Microsoft.Dafny {
       E0 = e0;

       E1 = e1;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Seq;

+        if (E0 != null) yield return E0;

+        if (E1 != null) yield return E1;

+      }

+    }

   }

 

   public class MultiSelectExpr : Expression {

@@ -1939,6 +1957,15 @@ namespace Microsoft.Dafny {
       Array = array;

       Indices = indices;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Array;

+        foreach (var e in Indices) {

+          yield return e;

+        }

+      }

+    }

   }

 

   public class SeqUpdateExpr : Expression {

@@ -1955,7 +1982,14 @@ namespace Microsoft.Dafny {
       Seq = seq;

       Index = index;

       Value = val;

+    }

 

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Seq;

+        yield return Index;

+        yield return Value;

+      }

     }

   }

 

@@ -1990,6 +2024,15 @@ namespace Microsoft.Dafny {
       this.Receiver = receiver;

       this.Args = args;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Receiver;

+        foreach (var e in Args) {

+          yield return e;

+        }

+      }

+    }

   }

 

   public class OldExpr : Expression {

@@ -2008,6 +2051,10 @@ namespace Microsoft.Dafny {
       cce.Owner.AssignSame(this, expr);

       E = expr;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get { yield return E; }

+    }

   }

 

   public class FreshExpr : Expression {

@@ -2023,6 +2070,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

       E = expr;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get { yield return E; }

+    }

   }

 

   public class AllocatedExpr : Expression

@@ -2039,6 +2090,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

       E = expr;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get { yield return E; }

+    }

   }

 

   public class UnaryExpr : Expression

@@ -2054,7 +2109,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(E != null);

     }

 

-

     public UnaryExpr(IToken tok, Opcode op, Expression e)

       : base(tok) {

       Contract.Requires(tok != null);

@@ -2063,6 +2117,10 @@ namespace Microsoft.Dafny {
       this.E = e;

 

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get { yield return E; }

+    }

   }

 

   public class BinaryExpr : Expression {

@@ -2195,7 +2253,13 @@ namespace Microsoft.Dafny {
       this.Op = op;

       this.E0 = e0;

       this.E1 = e1;

+    }

 

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return E0;

+        yield return E1;

+      }

     }

   }

 

@@ -2209,10 +2273,36 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Body != null);

     }

 

-

     public readonly Triggers Trigs;

     public readonly Attributes Attributes;

 

+    public abstract class BoundedPool { }

+    public class IntBoundedPool : BoundedPool

+    {

+      public readonly Expression LowerBound;

+      public readonly Expression UpperBound;

+      public IntBoundedPool(Expression lowerBound, Expression upperBound) {

+        LowerBound = lowerBound;

+        UpperBound = upperBound;

+      }

+    }

+    public class SetBoundedPool : BoundedPool

+    {

+      public readonly Expression Set;

+      public SetBoundedPool(Expression set) { Set = set; }

+    }

+    public class SeqBoundedPool : BoundedPool

+    {

+      public readonly Expression Seq;

+      public SeqBoundedPool(Expression seq) { Seq = seq; }

+    }

+    public class BoolBoundedPool : BoundedPool

+    {

+    }

+

+    public List<BoundedPool> Bounds;  // initialized and filled in by resolver; it remains null for quantifiers in specification contexts

+    // invariant bounds == null || bounds.Count == BoundVars.Count;

+

     public QuantifierExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression/*!*/ body, Triggers trigs, Attributes attrs)

       : base(tok) {

       Contract.Requires(tok != null);

@@ -2223,7 +2313,10 @@ namespace Microsoft.Dafny {
       this.Body = body;

       this.Trigs = trigs;

       this.Attributes = attrs;

+    }

 

+    public override IEnumerable<Expression> SubExpressions {

+      get { yield return Body; }

     }

   }

 

@@ -2264,7 +2357,6 @@ namespace Microsoft.Dafny {
     public WildcardExpr(IToken tok)

       : base(tok) {

       Contract.Requires(tok != null);

-

     }

   }

 

@@ -2279,7 +2371,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Els != null);

     }

 

-

     public ITEExpr(IToken tok, Expression test, Expression thn, Expression els)

       : base(tok) {

       Contract.Requires(tok != null);

@@ -2289,7 +2380,14 @@ namespace Microsoft.Dafny {
       this.Test = test;

       this.Thn = thn;

       this.Els = els;

+    }

 

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Test;

+        yield return Thn;

+        yield return Els;

+      }

     }

   }

 

@@ -2302,7 +2400,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(cce.NonNullElements(Cases));

     }

 

-

     public MatchExpr(IToken tok, Expression source, [Captured] List<MatchCaseExpr/*!*/>/*!*/ cases)

       : base(tok) {

       Contract.Requires(tok != null);

@@ -2310,8 +2407,15 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(cases));

       this.Source = source;

       this.Cases = cases;

+    }

 

-

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Source;

+        foreach (var mc in Cases) {

+          yield return mc.Body;

+        }

+      }

     }

   }

 

@@ -2368,7 +2472,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(ToType != null);

     }

 

-

     public BoxingCastExpr(Expression e, Type fromType, Type toType)

       : base(e.tok) {

       Contract.Requires(e != null);

@@ -2379,6 +2482,10 @@ namespace Microsoft.Dafny {
       FromType = fromType;

       ToType = toType;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get { yield return E; }

+    }

   }

 

   public class UnboxingCastExpr : Expression {  // an UnboxingCastExpr is used only as a temporary placeholding during translation

@@ -2392,7 +2499,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(ToType != null);

     }

 

-

     public UnboxingCastExpr(Expression e, Type fromType, Type toType)

       : base(e.tok) {

       Contract.Requires(e != null);

@@ -2403,6 +2509,10 @@ namespace Microsoft.Dafny {
       FromType = fromType;

       ToType = toType;

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get { yield return E; }

+    }

   }

 

   public class MaybeFreeExpression {

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 82cb6651..09bed6dd 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1091,8 +1091,10 @@ namespace Microsoft.Dafny {
       }

     }

     

-    public void ResolveStatement(Statement stmt, bool specContextOnly, Method method){Contract.Requires(stmt != null);Contract.Requires(method != null);

-     Contract.Requires(!(stmt is LabelStmt));  // these should be handled inside lists of statements

+    public void ResolveStatement(Statement stmt, bool specContextOnly, Method method) {

+      Contract.Requires(stmt != null);

+      Contract.Requires(method != null);

+      Contract.Requires(!(stmt is LabelStmt));  // these should be handled inside lists of statements

       if (stmt is UseStmt) {

         UseStmt s = (UseStmt)stmt;

         s.IsGhost = true;

@@ -2157,10 +2159,8 @@ namespace Microsoft.Dafny {
         

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

+        int prevErrorCount = ErrorCount;

         scope.PushMarker();

-        if (!specContext) {

-          Error(expr, "quantifiers are allowed only in specification contexts");

-        }

         foreach (BoundVar v in e.BoundVars) {

           if (!scope.Push(v.Name, v)) {

             Error(v, "Duplicate bound-variable name: {0}", v.Name);

@@ -2178,6 +2178,17 @@ namespace Microsoft.Dafny {
         ResolveTriggers(e.Trigs, twoState);

         scope.PopMarker();

         expr.Type = Type.Bool;

+

+        if (prevErrorCount == ErrorCount) {

+          if (specContext) {

+            // any quantifier is allowed

+          } else {

+            // ...but in non-spec contexts, it is necessary to compile the quantifier, so only certain quantifiers

+            // whose bound variables draw their values from bounded pools of values are allowed.  To check for such

+            // "bounded pools", this resolving code looks for certain patterns.

+            e.Bounds = DiscoverBounds(e);

+          }

+        }

         

       } else if (expr is WildcardExpr) {

         expr.Type = new SetType(new ObjectType());

@@ -2305,6 +2316,378 @@ namespace Microsoft.Dafny {
         expr.Type = Type.Flexible;

       }

     }

+

+    /// <summary>

+    /// Tries to find a bounded pool for each of the bound variables of "e".  If this process fails, appropriate

+    /// error messages are reported and "null" is returned.

+    /// Requires "e" to be successfully resolved.

+    /// </summary>

+    List<QuantifierExpr.BoundedPool> DiscoverBounds(QuantifierExpr e) {

+      Contract.Requires(e != null);

+      Contract.Requires(e.Type != null);  // a sanity check (but not a complete proof) that "e" has been resolved

+      Contract.Ensures(Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == e.BoundVars.Count);

+

+      var bounds = new List<QuantifierExpr.BoundedPool>();

+      for (int j = 0; j < e.BoundVars.Count; j++) {

+        var bv = e.BoundVars[j];

+        if (bv.Type == Type.Bool) {

+          // easy

+          bounds.Add(new QuantifierExpr.BoolBoundedPool());

+        } else {

+          // Go through the conjuncts of the range expression look for bounds.

+          Expression lowerBound = null;

+          Expression upperBound = null;

+          foreach (var conjunct in NormalizedConjuncts(e.Body, e is ExistsExpr)) {

+            var c = conjunct as BinaryExpr;

+            if (c == null) {

+              goto CHECK_NEXT_CONJUNCT;

+            }

+            var e0 = c.E0;

+            var e1 = c.E1;

+            var op = c.ResolvedOp;

+            int whereIsBv = SanitizeForBoundDiscovery(e.BoundVars, j, ref op, ref e0, ref e1);

+            if (whereIsBv < 0) {

+              goto CHECK_NEXT_CONJUNCT;

+            }

+            switch (op) {

+              case BinaryExpr.ResolvedOpcode.InSet:

+                if (whereIsBv == 0) {

+                  bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

+                  goto CHECK_NEXT_BOUND_VARIABLE;

+                }

+                break;

+              case BinaryExpr.ResolvedOpcode.InSeq:

+                if (whereIsBv == 0) {

+                  bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

+                  goto CHECK_NEXT_BOUND_VARIABLE;

+                }

+                break;

+              case BinaryExpr.ResolvedOpcode.EqCommon:

+                if (bv.Type == Type.Int) {

+                  var otherOperand = whereIsBv == 0 ? e1 : e0;

+                  bounds.Add(new QuantifierExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));

+                  goto CHECK_NEXT_BOUND_VARIABLE;

+                }

+                break;

+              case BinaryExpr.ResolvedOpcode.Gt:

+              case BinaryExpr.ResolvedOpcode.Ge:

+                Contract.Assert(false); throw new cce.UnreachableException();  // promised by postconditions of NormalizedConjunct and SanitizeForBoundDiscovery

+              case BinaryExpr.ResolvedOpcode.Lt:

+                if (whereIsBv == 0 && upperBound == null) {

+                  upperBound = e1;  // bv < E

+                } else if (whereIsBv == 1 && lowerBound == null) {

+                  lowerBound = Plus(e0, 1);  // E < bv

+                }

+                break;

+              case BinaryExpr.ResolvedOpcode.Le:

+                if (whereIsBv == 0 && upperBound == null) {

+                  upperBound = Plus(e1, 1);  // bv <= E

+                } else if (whereIsBv == 1 && lowerBound == null) {

+                  lowerBound = e0;  // E <= bv

+                }

+                break;

+              default:

+                break;

+            }

+            if (lowerBound != null && upperBound != null) {

+              // we have found two halves

+              bounds.Add(new QuantifierExpr.IntBoundedPool(lowerBound, upperBound));

+              goto CHECK_NEXT_BOUND_VARIABLE;

+            }

+          CHECK_NEXT_CONJUNCT: ;

+          }

+          // we have checked every conjunct in the range expression and still have not discovered good bounds

+          Error(e, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

+          return null;

+        }

+      CHECK_NEXT_BOUND_VARIABLE: ;  // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)

+      }

+      return bounds;

+    }

+

+    /// <summary>

+    /// If the return value is negative, the resulting "op", "e0", and "e1" should not be used.

+    /// Otherwise, the following is true on return:

+    /// The new "e0 op e1" is equivalent to the old "e0 op e1".

+    /// One of "e0" and "e1" is the identifier "boundVars[bvi]"; the return value is either 0 or 1, and indicates which.

+    /// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".

+    /// Requires the initial value of "op" not to be Gt or Ge, and ensures the same about the final value of "op".

+    /// </summary>

+    int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, ref BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1)

+    {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Requires(boundVars != null);

+      Contract.Requires(0 <= bvi && bvi < boundVars.Count);

+      Contract.Ensures(Contract.Result<int>() < 2);

+

+      var bv = boundVars[bvi];

+

+      // make an initial assessment of where bv is; to continue, we need bv to appear in exactly one operand

+      var fv0 = FreeVariables(e0);

+      var fv1 = FreeVariables(e1);

+      Expression thisSide;

+      Expression thatSide;

+      int whereIsBv;

+      if (fv0.Contains(bv)) {

+        if (fv1.Contains(bv)) {

+          return -1;

+        }

+        whereIsBv = 0;

+        thisSide = e0; thatSide = e1;

+      } else if (fv1.Contains(bv)) {

+        whereIsBv = 1;

+        thisSide = e1; thatSide = e0;

+      } else {

+        return -1;

+      }

+

+      // Next, clean up the side where bv is by adjusting both sides of the expression

+      while (true) {

+        switch (op) {

+          case BinaryExpr.ResolvedOpcode.EqCommon:

+          case BinaryExpr.ResolvedOpcode.NeqCommon:

+          case BinaryExpr.ResolvedOpcode.Gt:

+          case BinaryExpr.ResolvedOpcode.Ge:

+          case BinaryExpr.ResolvedOpcode.Le:

+          case BinaryExpr.ResolvedOpcode.Lt:

+            var bin = thisSide as BinaryExpr;

+            if (bin != null) {

+              if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {

+                // Change "A+B op C" into either "A op C-B" or "B op C-A", depending on where we find bv among A and B.

+                if (!FreeVariables(bin.E1).Contains(bv)) {

+                  thisSide = bin.E0;

+                  thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E1);

+                } else {

+                  thisSide = bin.E1;

+                  thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E0);

+                }

+                ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;

+                thatSide.Type = bin.Type;

+                continue;  // continue simplifying

+

+              } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub) {

+                // Change "A-B op C" in a similar way.

+                if (!FreeVariables(bin.E1).Contains(bv)) {

+                  // change to "A op C+B"

+                  thisSide = bin.E0;

+                  thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Add, thatSide, bin.E1);

+                  ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Add;

+                } else {

+                  // In principle, change to "-B op C-A" and then to "B dualOp A-C".  But since we don't want

+                  // to return with the operator being > or >=, we instead end with "A-C op B" and switch the

+                  // mapping of thisSide/thatSide to e0/e1 (by inverting "whereIsBv").

+                  thisSide = bin.E1;

+                  thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, bin.E0, thatSide);

+                  ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;

+                  whereIsBv = 1 - whereIsBv;

+                }

+                thatSide.Type = bin.Type;

+                continue;  // continue simplifying

+              }

+            }

+            break;  // done simplifying

+          default:

+            break;  // done simplifying

+        }

+        break;  // done simplifying

+      }

+

+      // Now, see if the interesting side is simply bv itself

+      if (thisSide is IdentifierExpr && ((IdentifierExpr)thisSide).Var == bv) {

+        // we're cool

+      } else {

+        // no, the situation is more complicated than we care to understand

+        return -1;

+      }

+

+      // Finally, check that the other side does not contain "bv" or any of the bound variables

+      // listed after "bv" in the quantifier.

+      var fv = FreeVariables(thatSide);

+      for (int i = bvi; i < boundVars.Count; i++) {

+        if (fv.Contains(boundVars[i])) {

+          return -1;

+        }

+      }

+

+      // As we return, also return the adjusted sides

+      if (whereIsBv == 0) {

+        e0 = thisSide; e1 = thatSide;

+      } else {

+        e0 = thatSide; e1 = thisSide;

+      }

+      return whereIsBv;

+    }

+

+    /// <summary>

+    /// Returns all conjuncts of "expr" in "polarity" positions.  That is, if "polarity" is "true", then

+    /// returns the conjuncts of "expr" in positive positions; else, returns the conjuncts of "expr" in

+    /// negative positions.  The method considers a canonical-like form of the expression that pushes

+    /// negations inwards far enough that one can determine what the result is going to be (so, almost

+    /// a negation normal form).

+    /// As a convenience, arithmetic inequalities are rewritten so that the negation of an arithmetic

+    /// inequality is never returned and the comparisons > and >= are never returned; the negation of

+    /// a common equality or disequality is rewritten analogously.

+    /// Requires "expr" to be successfully resolved.

+    /// </summary>

+    IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {

+      // We consider 5 cases.  To describe them, define P(e)=Conjuncts(e,true) and N(e)=Conjuncts(e,false).

+      //   *  X ==> Y    is treated as a shorthand for !X || Y, and so is described by the remaining cases

+      //   *  X && Y     P(_) = P(X),P(Y)    and    N(_) = !(X && Y)

+      //   *  X || Y     P(_) = (X || Y)     and    N(_) = N(X),N(Y)

+      //   *  !X         P(_) = N(X)         and    N(_) = P(X)

+      //   *  else       P(_) = else         and    N(_) = !else

+      // So for ==>, we have:

+      //   *  X ==> Y    P(_) = P(!X || Y) = (!X || Y) = (X ==> Y)

+      //                 N(_) = N(!X || Y) = N(!X),N(Y) = P(X),N(Y)

+

+      // Binary expressions

+      var b = expr as BinaryExpr;

+      if (b != null) {

+        bool breakDownFurther = false;

+        bool p0 = polarity;

+        if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {

+          breakDownFurther = polarity;

+        } else if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {

+          breakDownFurther = !polarity;

+        } else if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {

+          breakDownFurther = !polarity;

+          p0 = !p0;

+        }

+        if (breakDownFurther) {

+          foreach (var c in NormalizedConjuncts(b.E0, p0)) {

+            yield return c;

+          }

+          foreach (var c in NormalizedConjuncts(b.E1, polarity)) {

+            yield return c;

+          }

+          yield break;

+        }

+      }

+

+      // Unary expression

+      var u = expr as UnaryExpr;

+      if (u != null && u.Op == UnaryExpr.Opcode.Not) {

+        foreach (var c in NormalizedConjuncts(u.E, !polarity)) {

+          yield return c;

+        }

+        yield break;

+      }

+

+      // no other case applied, so return the expression or its negation, but first clean it up a little

+      b = expr as BinaryExpr;

+      if (b != null) {

+        BinaryExpr.Opcode newOp;

+        BinaryExpr.ResolvedOpcode newROp;

+        bool swapOperands;

+        switch (b.ResolvedOp) {

+          case BinaryExpr.ResolvedOpcode.Gt:  // A > B         yield polarity ? (B < A) : (A <= B);

+            newOp = polarity ? BinaryExpr.Opcode.Lt : BinaryExpr.Opcode.Le;

+            newROp = polarity ? BinaryExpr.ResolvedOpcode.Lt : BinaryExpr.ResolvedOpcode.Le;

+            swapOperands = polarity;

+            break;

+          case BinaryExpr.ResolvedOpcode.Ge:  // A >= B        yield polarity ? (B <= A) : (A < B);

+            newOp = polarity ? BinaryExpr.Opcode.Le : BinaryExpr.Opcode.Lt;

+            newROp = polarity ? BinaryExpr.ResolvedOpcode.Le : BinaryExpr.ResolvedOpcode.Lt;

+            swapOperands = polarity;

+            break;

+          case BinaryExpr.ResolvedOpcode.Le:  // A <= B        yield polarity ? (A <= B) : (B < A);

+            newOp = polarity ? BinaryExpr.Opcode.Le : BinaryExpr.Opcode.Lt;

+            newROp = polarity ? BinaryExpr.ResolvedOpcode.Le : BinaryExpr.ResolvedOpcode.Lt;

+            swapOperands = !polarity;

+            break;

+          case BinaryExpr.ResolvedOpcode.Lt:  // A < B         yield polarity ? (A < B) : (B <= A);

+            newOp = polarity ? BinaryExpr.Opcode.Lt : BinaryExpr.Opcode.Le;

+            newROp = polarity ? BinaryExpr.ResolvedOpcode.Lt : BinaryExpr.ResolvedOpcode.Le;

+            swapOperands = !polarity;

+            break;

+          case BinaryExpr.ResolvedOpcode.EqCommon:  // A == B         yield polarity ? (A == B) : (A != B);

+            newOp = polarity ? BinaryExpr.Opcode.Eq : BinaryExpr.Opcode.Neq;

+            newROp = polarity ? BinaryExpr.ResolvedOpcode.EqCommon : BinaryExpr.ResolvedOpcode.NeqCommon;

+            swapOperands = false;

+            break;

+          case BinaryExpr.ResolvedOpcode.NeqCommon:  // A != B         yield polarity ? (A != B) : (A == B);

+            newOp = polarity ? BinaryExpr.Opcode.Neq : BinaryExpr.Opcode.Eq;

+            newROp = polarity ? BinaryExpr.ResolvedOpcode.NeqCommon : BinaryExpr.ResolvedOpcode.EqCommon;

+            swapOperands = false;

+            break;

+          default:

+            goto JUST_RETURN_IT;

+        }

+        if (newROp != b.ResolvedOp || swapOperands) {

+          b = new BinaryExpr(b.tok, newOp, swapOperands ? b.E1 : b.E0, swapOperands ? b.E0 : b.E1);

+          b.ResolvedOp = newROp;

+          b.Type = Type.Bool;

+          yield return b;

+        }

+      }

+    JUST_RETURN_IT: ;

+      if (polarity) {

+        yield return expr;

+      } else {

+        expr = new UnaryExpr(expr.tok, UnaryExpr.Opcode.Not, expr);

+        expr.Type = Type.Bool;

+        yield return expr;

+      }

+    }

+

+    Expression Plus(Expression e, int n) {

+      Contract.Requires(0 <= n);

+

+      var nn = new LiteralExpr(e.tok, n);

+      nn.Type = Type.Int;

+      var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Add, e, nn);

+      p.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;

+      p.Type = Type.Int;

+      return p;

+    }

+

+    /// <summary>

+    /// Returns the set of free variables in "expr".

+    /// Requires "expr" to be successfully resolved.

+    /// Ensures that the set returned has no aliases.

+    /// </summary>

+    ISet<IVariable> FreeVariables(Expression expr) {

+      Contract.Requires(expr != null);

+      Contract.Ensures(expr.Type != null);

+

+      if (expr is IdentifierExpr) {

+        var e = (IdentifierExpr)expr;

+        return new HashSet<IVariable>() { e.Var };

+

+      } else  if (expr is QuantifierExpr) {

+        var e = (QuantifierExpr)expr;

+        var s = FreeVariables(e.Body);

+        foreach (var bv in e.BoundVars) {

+          s.Remove(bv);

+        }

+        return s;

+

+      } else if (expr is MatchExpr) {

+        var e = (MatchExpr)expr;

+        var s = FreeVariables(e.Source);

+        foreach (MatchCaseExpr mc in e.Cases) {

+          var t = FreeVariables(mc.Body);

+          foreach (var bv in mc.Arguments) {

+            t.Remove(bv);

+          }

+          s.UnionWith(t);

+        }

+        return s;

+

+      } else {

+        ISet<IVariable> s = null;

+        foreach (var e in expr.SubExpressions) {

+          var t = FreeVariables(e);

+          if (s == null) {

+            s = t;

+          } else {

+            s.UnionWith(t);

+          }

+        }

+        return s == null ? new HashSet<IVariable>() : s;

+      }

+    }

     

     void ResolveReceiver(Expression expr, bool twoState, bool specContext)

     {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index b641b69d..a480d2c4 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -1290,7 +1290,12 @@ namespace Microsoft.Dafny {
 

         // check that postconditions hold

         foreach (Expression p in f.Ens) {

-          bodyCheckBuilder.Add(Assert(p.tok, etran.TrExpr(p), "possible violation of function postcondition"));

+          bool splitHappened;

+          foreach (var s in TrSplitExpr(p, etran, out splitHappened)) {

+            if (!s.IsFree) {

+              bodyCheckBuilder.Add(Assert(s.E.tok, s.E, "possible violation of function postcondition"));

+            }

+          }

         }

       }

       // Combine the two

@@ -3294,18 +3299,15 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr.Type is BoolType);

       Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<Expression>>()));

 

-      if (expr is BinaryExpr) {

-        BinaryExpr bin = (BinaryExpr)expr;

-        if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {

-          foreach (Expression e in Conjuncts(bin.E0)) {

-            yield return e;

-          }

-          Contract.Assert(bin != null);  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one

-          foreach (Expression e in Conjuncts(bin.E1)) {

-            yield return e;

-          }

-          yield break;

+      var bin = expr as BinaryExpr;

+      if (bin != null && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {

+        foreach (Expression e in Conjuncts(bin.E0)) {

+          yield return e;

+        }

+        foreach (Expression e in Conjuncts(bin.E1)) {

+          yield return e;

         }

+        yield break;

       }

       yield return expr;

     }

@@ -5068,20 +5070,60 @@ namespace Microsoft.Dafny {
 

       for (var a = e.Attributes; a != null; a = a.Prev) {

         if (a.Name == "induction") {

-          // return 'true', except if there is one argument and it is 'false'

+          // Here are the supported forms of the :induction attribute.

+          //    :induction           -- apply induction to all bound variables

+          //    :induction false     -- suppress induction, that is, don't apply it to any bound variable

+          //    :induction L       where L is a list consisting entirely of bound variables:

+          //                         -- apply induction to the specified bound variables

+          //    :induction X       where X is anything else

+          //                         -- treat the same as {:induction}, that is, apply induction to all

+          //                            bound variables

+

+          // Handle {:induction false}

           if (a.Args.Count == 1) {

             var arg = a.Args[0].E as LiteralExpr;

             if (arg != null && arg.Value is bool && !(bool)arg.Value) {

               if (CommandLineOptions.Clo.Trace) {

-                Console.Write("Suppressing automatic induction on: ");

+                Console.Write("Suppressing automatic induction for: ");

                 new Printer(Console.Out).PrintExpression(e);

                 Console.WriteLine();

               }

               return new List<BoundVar>();

             }

           }

+

+          // Handle {:induction L}

+          if (a.Args.Count != 0) {

+            var L = new List<BoundVar>();

+            foreach (var arg in a.Args) {

+              var id = arg.E as IdentifierExpr;

+              var bv = id == null ? null : id.Var as BoundVar;

+              if (bv != null && e.BoundVars.Contains(bv)) {

+                // add to L, but don't add duplicates

+                if (!L.Contains(bv)) {

+                  L.Add(bv);

+                }

+              } else {

+                goto USE_DEFAULT_FORM;

+              }

+            }

+            if (CommandLineOptions.Clo.Trace) {

+              string sep = "Applying requested induction on ";

+              foreach (var bv in L) {

+                Console.Write("{0}{1}", sep, bv.Name);

+                sep = ", ";

+              }

+              Console.Write(" of: ");

+              new Printer(Console.Out).PrintExpression(e);

+              Console.WriteLine();

+            }

+            return L;

+          USE_DEFAULT_FORM: ;

+          }

+

+          // We have the {:induction} case, or something to be treated in the same way

           if (CommandLineOptions.Clo.Trace) {

-            Console.Write("Applying requested induction on: ");

+            Console.Write("Applying requested induction on all bound variables of: ");

             new Printer(Console.Out).PrintExpression(e);

             Console.WriteLine();

           }

diff --git a/Test/VSComp2010/Answer b/Test/VSComp2010/Answer
index 50f20679..dc523fdf 100644
--- a/Test/VSComp2010/Answer
+++ b/Test/VSComp2010/Answer
@@ -16,7 +16,7 @@ Compiled program written to out.cs
 

 -------------------- Problem4-Queens.dfy --------------------

 

-Dafny program verifier finished with 11 verified, 0 errors

+Dafny program verifier finished with 9 verified, 0 errors

 Compiled program written to out.cs

 

 -------------------- Problem5-DoubleEndedQueue.dfy --------------------

diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy
index e73c644f..ef084674 100644
--- a/Test/VSComp2010/Problem4-Queens.dfy
+++ b/Test/VSComp2010/Problem4-Queens.dfy
@@ -1,5 +1,5 @@
 // VSComp 2010, problem 4, N queens

-// Rustan Leino, 31 August 2010.

+// Rustan Leino, 31 August 2010, updated 24 March 2011.

 //

 // In the version of this program that I wrote during the week of VSTTE 2010, I had

 // an unproved assumption.  In this version, I simply changed the existential quantifier

@@ -11,17 +11,7 @@
 // The correctness of this program relies on some properties of Queens boards.  These

 // are stated and proved as lemmas, which here are given in assert statements.

 //

-// There are two annoyances in this program:

-//

-// One has to do with Dafny's split between ''ghost'' variables/code and ''physical''

-// variables/code.  The ''ghost'' things are used by the verifier, but are ignored by

-// the compiler.  This is generally good, since any additional specifications are ghost

-// state that are needed to convince the verifier that a program is correct (let alone

-// express what it means for the program to be correct) are not required at run time.

-// However, Dafny currently considers *all* quantifiers to be ghost-only, which

-// necessitates some duplication of the 'IsConsistent' condition.

-//

-// The other annoyance is that Dafny's proof-term representation of the function

+// There is an annoyance in this program.  Dafny's proof-term representation of the function

 // 'IsConsistent' implicitly takes the heap as an argument, despite the fact that

 // 'IsConsistent' does not depend on any part of the heap.  Dafny ought to be able

 // to figure that out from the fact that 'IsConsistent' has no 'reads' clause.

@@ -29,6 +19,10 @@
 // below are specified with an (easy-to-prove) postcondition that 'IsConsistent(B,p)'

 // does not change for any 'B' and 'p', even if the method may change the heap in

 // some way.

+//

+// The March 2011 update of this program was to make use of Dafny's new heuristics for

+// compiling quantifiers.  This makes it possible to call IsConsistent, whose body uses

+// a universal quantifier, from non-ghost code, which simplifies this program.

 

 

 // The Search method returns whether or not there exists an N-queens solution for the

@@ -50,7 +44,7 @@ method Search(N: int) returns (success: bool, board: seq<int>)
 

 // Given a board, this function says whether or not the queen placed in column 'pos'

 // is consistent with the queens placed in columns to its left.

-static function IsConsistent(board: seq<int>, pos: int): bool

+static function method IsConsistent(board: seq<int>, pos: int): bool

 {

   0 <= pos && pos < |board| &&

   (forall q :: 0 <= q && q < pos ==>

@@ -59,37 +53,6 @@ static function IsConsistent(board: seq<int>, pos: int): bool
       board[pos] - board[q] != pos - q)

 }

 

-method CheckConsistent(board: seq<int>, pos: int) returns (b: bool)

-  ensures b <==> IsConsistent(board, pos);

-  ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p)));

-{

-  // The Dafny compiler won't compile a function with a 'forall' inside.  (This seems reasonable

-  // in general, since quantifiers could range over all the integers.  Here, however, where the

-  // range of the quantifier is bounded, it just seems stupid.)  Therefore, we

-  // have to provide a method that computes the same thing as the function defines.

-  if (0 <= pos && pos < |board|) {

-    var p := 0;

-    while (p < pos)

-      invariant p <= pos;

-      invariant (forall q :: 0 <= q && q < p ==>

-                  board[q] != board[pos] &&

-                  board[q] - board[pos] != pos - q &&

-                  board[pos] - board[q] != pos - q);

-    {

-      if (!(board[p] != board[pos] &&

-            board[p] - board[pos] != pos - p &&

-            board[pos] - board[p] != pos - p)) {

-        b := false;

-        return;

-      }

-      p := p + 1;

-    }

-    b := true;

-    return;

-  }

-  b := false;

-}

-

 // Here comes the method where the real work is being done.  With an ultimate board size of 'N'

 // in mind and given the consistent placement 'boardSoFar' of '|boardSoFar|' columns, this method

 // will search for a solution for the remaining columns.  If 'success' returns as 'true',

@@ -135,8 +98,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
     {

       // Let's try to extend the board-so-far with a queen in column 'n':

       var candidateBoard := boardSoFar + [n];

-      call consistent := CheckConsistent(candidateBoard, pos);

-      if (consistent) {

+      if (IsConsistent(candidateBoard, pos)) {

         // The new queen is consistent.  Thus, 'candidateBoard' is consistent in column 'pos'.

         // The consistency of the queens in columns left of 'pos' follows from the

         // consistency of those queens in 'boardSoFar' and the fact that 'candidateBoard' is

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c33cf851..b1e12099 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -295,7 +295,7 @@ Execution trace:
     Definedness.dfy(208,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(231,30): Error: possible violation of function postcondition

+Definedness.dfy(231,46): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

@@ -321,7 +321,7 @@ Execution trace:
     (0,0): anon13_Else

     (0,0): anon7

     (0,0): anon9

-FunctionSpecifications.dfy(40,18): Error: possible violation of function postcondition

+FunctionSpecifications.dfy(40,24): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon12_Else

     (0,0): anon15_Else

@@ -399,6 +399,16 @@ Execution trace:
 

 Dafny program verifier finished with 8 verified, 2 errors

 

+-------------------- NonGhostQuantifiers.dfy --------------------

+NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

+NonGhostQuantifiers.dfy(57,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'

+NonGhostQuantifiers.dfy(61,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

+NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

+NonGhostQuantifiers.dfy(86,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

+NonGhostQuantifiers.dfy(94,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

+NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

+7 resolution/type errors detected in NonGhostQuantifiers.dfy

+

 -------------------- Modules0.dfy --------------------

 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

 Modules0.dfy(13,7): Error: module T named among imports does not exist

diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy
new file mode 100644
index 00000000..dd730e90
--- /dev/null
+++ b/Test/dafny0/NonGhostQuantifiers.dfy
@@ -0,0 +1,125 @@
+// This file contains various tests of resolving quantifiers in ghost and non-ghost positions

+

+class MyClass<T> {

+  // This function is in a ghost context, so all is cool.

+  function GhostF(): bool

+  {

+    (forall n :: 2 <= n ==> (exists d :: n < d && d < 2*n))

+  }

+  // But try to make it a non-ghost function, and Dafny will object because it cannot compile the

+  // body into code that will terminate.

+  function method NonGhostF(): bool

+  {

+    (forall n :: 2 <= n ==> (exists d :: n < d && d < 2*n))  // error: can't figure out how to compile

+  }

+  // Add an upper bound to n and things are cool again.

+  function method NonGhostF_Bounded(): bool

+  {

+    (forall n :: 2 <= n && n < 1000 ==> (exists d :: n < d && d < 2*n))

+  }

+  // Although the heuristics applied are syntactic, they do see through the structure of the boolean

+  // operators ==>, &&, ||, and !.  Hence, the following three variations of the previous function can

+  // also be compiled.

+  function method NonGhostF_Or(): bool

+  {

+    (forall n :: !(2 <= n && n < 1000) || (exists d :: n < d && d < 2*n))

+  }

+  function method NonGhostF_ImpliesImplies(): bool

+  {

+    (forall n :: 2 <= n ==> n < 1000 ==> (exists d :: n < d && d < 2*n))

+  }

+  function method NonGhostF_Shunting(): bool

+  {

+    (forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))

+  }

+

+  // Here are more tests

+

+  function method F(a: array<T>): bool

+    requires a != null;

+    reads a;

+  {

+    (exists i :: 0 <= i && i < a.Length / 2 && (forall j :: i <= j && j < a.Length ==> a[i] == a[j]))

+  }

+

+  function method G0(a: seq<T>): bool

+  {

+    (exists t :: t in a && (forall u :: u in a ==> u == t))

+  }

+  function method G1(a: seq<T>): bool

+  {

+    (exists ti :: 0 <= ti && ti < |a| && (forall ui :: 0 <= ui && ui < |a| ==> a[ui] == a[ti]))

+  }

+

+  // Regrettably, the heuristics don't know about transitivity:

+  function method IsSorted0(s: seq<int>): bool

+  {

+    (forall i, j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j])  // error: can't figure out how to compile

+  }

+  function method IsSorted1(s: seq<int>): bool

+  {

+    (forall j, i :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j])  // error: can't figure out how to compile

+  }

+  // Add the redundant conjunct "i < |s|" and things are fine.

+  function method IsSorted2(s: seq<int>): bool

+  {

+    (forall i, j :: 0 <= i && i < |s| && i < j && j < |s| ==> s[i] <= s[j])

+  }

+  // But if you switch the order of i and j, you need a different redundant conjunct.

+  function method IsSorted3(s: seq<int>): bool

+  {

+    (forall j, i :: 0 <= i && i < |s| && i < j && j < |s| ==> s[i] <= s[j])  // error: can't figure out how to compile

+  }

+  function method IsSorted4(s: seq<int>): bool

+  {

+    (forall j, i  :: 0 <= i && 0 < j && i < j && j < |s| ==> s[i] <= s[j])

+  }

+

+  // The heuristics look at bound variables in the order given, as is illustrated by the following

+  // two functions.

+  function method Order0(S: seq<set<int>>): bool

+  {

+    (forall i, j :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j)

+  }

+  function method Order1(S: seq<set<int>>): bool

+  {

+    (forall j, i :: 0 <= i && i < |S| && j in S[i] ==> 0 <= j)  // error: can't figure out how to compile

+  }

+

+  // Quantifiers can be used in other contexts, too.

+  // For example, in assert statements and assignment statements.

+  method M(s: seq<int>) returns (r: bool, q: bool) {

+    assert (forall x :: x in s ==> 0 <= x);

+    r := (forall x :: x in s ==> x < 100);

+    q := (exists y :: y*y in s);  // error: can't figure out how to compile

+  }

+  // And if expressions.

+  function method Select_Good(S: set<int>, a: T, b: T): T

+  {

+    if (forall x :: x in S ==> 0 <= x && x < 100) then a else b

+  }

+  function method Select_Bad(S: set<int>, a: T, b: T): T

+  {

+    if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b  // error: can't figure out how to compile

+  }

+  // (the same thing, but in a ghost function is fine, though)

+  function Select_Bad_Ghost(S: set<int>, a: T, b: T): T

+  {

+    if (forall x :: x*x in S ==> 0 <= x && x < 100) then a else b

+  }

+  // And if statements

+/****

+  method N(s: seq<int>) returns (ghost g: int, h: int)

+  {

+    if ( (forall x :: x in s ==> 0 <= x) ) {

+      h := 0;  g := 0;

+    }

+    if ( (forall x :: x*x in s ==> x < 100) ) {  // this is fine, since the whole statement is a ghost statement

+      g := 2;

+    }

+    if ( (forall x :: x*x in s ==> x < 50) ) {  // error: cannot compile this guard of a non-ghost if statement

+      h := 6;

+    }

+  }

+****/

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 3e9507ef..2c55a6b9 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -12,7 +12,7 @@ for %%f in (Simple.dfy) do (
 )

 

 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy

-            Array.dfy MultiDimArray.dfy

+            Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 4bf200cd..d9b32305 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -73,7 +73,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 

 -------------------- Induction.dfy --------------------

 

-Dafny program verifier finished with 22 verified, 0 errors

+Dafny program verifier finished with 23 verified, 0 errors

 

 -------------------- Rippling.dfy --------------------

 

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 4bd1f35b..f31d79f8 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -107,6 +107,25 @@ class IntegerInduction {
       call Theorem4();

     }

   }

+

+  // The body of this function method gives a single quantifier, which leads to an efficient

+  // way to check sortedness at run time.  However, an alternative, and ostensibly more general,

+  // way to express sortedness is given in the function's postcondition.  The alternative

+  // formulation may be easier to understand for a human and may also be more readily applicable

+  // for the program verifier.  Dafny will show that postcondition holds, which ensures the

+  // equivalence of the two formulations.

+  // The proof of the postcondition requires induction.  It would have been nicer to state it

+  // as one formula of the form "IsSorted(s) <==> ...", but then Dafny would never consider the

+  // possibility of applying induction.  Instead, the "==>" and "<==" cases are given separately.

+  // Proving the "<==" case is simple; it's the "==>" case that requires induction.

+  // The example uses an attribute that requests induction on just "j".  However, the proof also

+  // goes through by applying induction just on "i" or applying induction on both bound variables.

+  function method IsSorted(s: seq<int>): bool

+    ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);

+    ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);

+  {

+    (forall i :: 0 <= i && i+1 < |s| ==> s[i] <= s[i+1])

+  }

 }

 

 datatype Tree<T> {