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

8 files changed, 608 insertions, 36 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 12264c95..e68c1b71 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -25,7 +25,7 @@ namespace Microsoft.Boogie {
     public static string/*!*/ VersionSuffix {

       get {

         Contract.Ensures(Contract.Result<string>() != null);

-        return " version " + VersionNumber + ", Copyright (c) 2003-2010, Microsoft.";

+        return " version " + VersionNumber + ", Copyright (c) 2003-2011, Microsoft.";

       }

     }

     public string/*!*/ InputFileExtension {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index dc7caac7..decc5223 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/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/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index a8acb013..b26e1288 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/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/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 82cb6651..09bed6dd 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/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/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b641b69d..a480d2c4 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/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/Source/Model/Properties/AssemblyInfo.cs b/Source/Model/Properties/AssemblyInfo.cs
index 2efc049f..80c3907a 100644
--- a/Source/Model/Properties/AssemblyInfo.cs
+++ b/Source/Model/Properties/AssemblyInfo.cs
@@ -10,7 +10,7 @@ using System.Runtime.InteropServices;
 [assembly: AssemblyConfiguration("")]

 [assembly: AssemblyCompany("Microsoft")]

 [assembly: AssemblyProduct("Model")]

-[assembly: AssemblyCopyright("Copyright © Microsoft 2010")]

+[assembly: AssemblyCopyright("Copyright © Microsoft 2010-2011")]

 [assembly: AssemblyTrademark("")]

 [assembly: AssemblyCulture("")]

 

diff --git a/Source/ModelViewer/Properties/AssemblyInfo.cs b/Source/ModelViewer/Properties/AssemblyInfo.cs
index a5ed6580..0cb39b63 100644
--- a/Source/ModelViewer/Properties/AssemblyInfo.cs
+++ b/Source/ModelViewer/Properties/AssemblyInfo.cs
@@ -10,7 +10,7 @@ using System.Runtime.InteropServices;
 [assembly: AssemblyConfiguration("")]

 [assembly: AssemblyCompany("Microsoft")]

 [assembly: AssemblyProduct("ModelViewer")]

-[assembly: AssemblyCopyright("Copyright © Microsoft 2010")]

+[assembly: AssemblyCopyright("Copyright © Microsoft 2010-2011")]

 [assembly: AssemblyTrademark("")]

 [assembly: AssemblyCulture("")]

 

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 616575db..93adec82 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -327,6 +327,7 @@ namespace Microsoft.Boogie.TypeErasure {
     public readonly Type/*!*/ T;

 

     public abstract Type/*!*/ TypeAfterErasure(Type/*!*/ type);

+    [Pure]

     public abstract bool UnchangedType(Type/*!*/ type);

 

     ///////////////////////////////////////////////////////////////////////////