Invert LHS sub-expressions in forall assignment statements, which gives the opportunity to designate a good trigger.

6 files changed, 474 insertions, 32 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 93e39ae6..44f9742b 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4128,6 +4128,20 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

+    /// Create a resolved expression of the form "e0 + e1"

+    /// </summary>

+    public static Expression CreateAdd(Expression e0, Expression e1) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Requires((e0.Type is IntType && e1.Type is IntType) || (e0.Type is RealType && e1.Type is RealType));

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

+      var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add, e0, e1);

+      s.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;  // resolve here

+      s.Type = e0.Type;  // resolve here

+      return s;

+    }

+

+    /// <summary>

     /// Create a resolved expression of the form "e0 - e1"

     /// </summary>

     public static Expression CreateSubtract(Expression e0, Expression e1) {

@@ -4152,12 +4166,8 @@ namespace Microsoft.Dafny {
       if (n == 0) {

         return e;

       }

-      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;

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

+      return CreateAdd(e, nn);

     }

 

     /// <summary>

@@ -4171,11 +4181,8 @@ namespace Microsoft.Dafny {
       if (n == 0) {

         return e;

       }

-      var nn = Expression.CreateIntLiteral(e.tok, n);

-      var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Sub, e, nn);

-      p.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;

-      p.Type = Type.Int;

-      return p;

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

+      return CreateSubtract(e, nn);

     }

 

     /// <summary>

@@ -4239,6 +4246,26 @@ namespace Microsoft.Dafny {
       return s;

     }

 

+    public static Expression CreateEq(Expression e0, Expression e1, Type ty) {

+      Contract.Requires(e0 != null);

+      Contract.Requires(e1 != null);

+      Contract.Requires(ty != null);

+      var eq = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Eq, e0, e1);

+      if (ty is SetType) {

+        eq.ResolvedOp = BinaryExpr.ResolvedOpcode.SetEq;

+      } else if (ty is SeqType) {

+        eq.ResolvedOp = BinaryExpr.ResolvedOpcode.SeqEq;

+      } else if (ty is MultiSetType) {

+        eq.ResolvedOp = BinaryExpr.ResolvedOpcode.InMultiSet;

+      } else if (ty is MapType) {

+        eq.ResolvedOp = BinaryExpr.ResolvedOpcode.MapEq;

+      } else {

+        eq.ResolvedOp = BinaryExpr.ResolvedOpcode.EqCommon;

+      }

+      eq.type = Type.Bool;

+      return eq;

+    }

+

     /// <summary>

     /// Create a resolved expression of the form "e0 && e1"

     /// </summary>

@@ -4370,6 +4397,17 @@ namespace Microsoft.Dafny {
       return q;

     }

 

+    /// <summary>

+    /// Create a resolved IdentifierExpr (whose token is that of the variable)

+    /// </summary>

+    public static Expression CreateIdentExpr(IVariable v) {

+      Contract.Requires(v != null);

+      var e = new IdentifierExpr(v.Tok, v.Name);

+      e.Var = v;  // resolve here

+      e.type = v.Type;  // resolve here

+      return e;

+    }

+

     public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e) {

       Contract.Requires(oldVars != null && newVars != null);

       Contract.Requires(oldVars.Count == newVars.Count);

@@ -4983,6 +5021,18 @@ namespace Microsoft.Dafny {
     public ResolvedOpcode ResolvedOp_PossiblyStillUndetermined {  // offer a way to return _theResolveOp -- for experts only!

       get { return _theResolvedOp; }

     }

+    public static bool IsEqualityOp(ResolvedOpcode op) {

+      switch (op) {

+        case ResolvedOpcode.EqCommon:

+        case ResolvedOpcode.SetEq:

+        case ResolvedOpcode.SeqEq:

+        case ResolvedOpcode.MultiSetEq:

+        case ResolvedOpcode.MapEq:

+          return true;

+        default:

+          return false;

+      }

+    }

 

     public static Opcode ResolvedOp2SyntacticOp(ResolvedOpcode rop) {

       switch (rop) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index ff3918df..479dac39 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5703,15 +5703,33 @@ namespace Microsoft.Dafny {
       //     assume $HeapSucc(oldHeap, $Heap);

       //     (a)

       //       assume (forall<alpha> o: ref, F: Field alpha ::

+      //         { $Heap[o,F] }

       //         $Heap[o,F] = oldHeap[o,F] ||

       //         (exists x,y :: Range(x,y) && o == E(x,y) && F = f));

-      //       assume (forall x,y ::  Range ==> $Heap[ E[$Heap:=oldHeap], F] == G[$Heap:=oldHeap]);

+      //       assume (forall x,y ::  Range ==> $Heap[ E[$Heap:=oldHeap], F] == G[$Heap:=oldHeap]); (**)

       //     (b)

       //       assume (forall<alpha> o: ref, F: Field alpha ::

+      //         { $Heap[o,F] }

       //         $Heap[o,F] = oldHeap[o,F] ||

       //         (exists x,y :: Range(x,y) && o == A(x,y) && F = Index(I0,I1,...)));

-      //       assume (forall x,y ::  Range ==> $Heap[ A[$Heap:=oldHeap], Index(I0,I1,...)] == G[$Heap:=oldHeap]);

+      //       assume (forall x,y ::  Range ==> $Heap[ A[$Heap:=oldHeap], Index(I0,I1,...)] == G[$Heap:=oldHeap]); (**)

       //   }

+      //

+      // Note: In order to get a good trigger for the quantifiers (**), we will attempt to make the parameters

+      // that select from $Heap in the LHS of the equalities as plain as possible.  This involves taking the inverse

+      // of an expression, which isn't always easy or possible, so we settle for handling some common cases.  In

+      // particular, we change:

+      //   0: forall i | R(i) { F(i).f := E(i); }

+      //   1: forall i | R(i) { A[F(i)] := E(i); }

+      //   2: forall i | R(i) { F(i)[N] := E(i); }

+      // where f is some field and A and N are expressions that do not depend on i, into:

+      //   0: forall j | Q(j) { j.f := E(F-1(j)); }

+      //   1: forall j | Q(j) { A[j] := E(F-1(j)); }

+      //   2: forall j | Q(j) { j[N] := E(F-1(j)); }

+      // where we ensure that, for all i and j:

+      //   R(i) && j == F(i)    <==>    Q(j) && F-1(j) == i

+      // If the transformation succeeds, we use, respectively, j.f, A[j], and j[N] (each evaluated in the new heap) as

+      // the trigger of the quantifier generated.

 

       var substMap = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);

       Expression range = Substitute(s.Range, null, substMap);

@@ -5777,6 +5795,7 @@ namespace Microsoft.Dafny {
 

       // Here comes:

       //   assume (forall<alpha> o: ref, f: Field alpha ::

+      //     { $Heap[o,f] }

       //     $Heap[o,f] = oldHeap[o,f] ||

       //     (exists x,y :: Range(x,y)[$Heap:=oldHeap] &&

       //                    o == Object(x,y)[$Heap:=oldHeap] && f == Field(x,y)[$Heap:=oldHeap]));

@@ -5796,30 +5815,249 @@ namespace Microsoft.Dafny {
       xBody = BplAnd(xBody, Bpl.Expr.Eq(f, xField));

       Bpl.Expr xObjField = new Bpl.ExistsExpr(s.Tok, xBvars, xBody);

       Bpl.Expr body = Bpl.Expr.Or(Bpl.Expr.Eq(heapOF, oldHeapOF), xObjField);

-      Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar }, body);

+      var tr = new Trigger(s.Tok, true, new List<Expr>() { heapOF });

+      Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar }, null, tr, body);

       updater.Add(new Bpl.AssumeCmd(s.Tok, qq));

 

       if (s0.Rhs is ExprRhs) {

-        //   assume (forall x,y :: Range(x,y)[$Heap:=oldHeap] ==>

-        //                         $Heap[ Object(x,y)[$Heap:=oldHeap], Field(x,y)[$Heap:=oldHeap] ] == G[$Heap:=oldHeap] ));

-        xBvars = new List<Variable>();

-        Bpl.Expr xAnte = etran.TrBoundVariables(s.BoundVars, xBvars);

-        xAnte = BplAnd(xAnte, prevEtran.TrExpr(s.Range));

+        Expression Fi = null;

+        Func<Expression,Expression> lhsBuilder = null;

+        lhs = s0.Lhs.Resolved;

+        var i = s.BoundVars[0];

+        if (s.BoundVars.Count == 1) {

+          //var lhsContext = null;

+          // Detect the following cases:

+          //   0: forall i | R(i) { F(i).f := E(i); }

+          //   1: forall i | R(i) { A[F(i)] := E(i); }

+          //   2: forall i | R(i) { F(i)[N] := E(i); }

+          if (lhs is FieldSelectExpr) {

+            var ll = (FieldSelectExpr)lhs;

+            Fi = ll.Obj;

+            lhsBuilder = e => { var l = new FieldSelectExpr(ll.tok, e, ll.FieldName); l.Field = ll.Field; l.Type = ll.Type; return l; };

+          } else if (lhs is SeqSelectExpr) {

+            var ll = (SeqSelectExpr)lhs;

+            Contract.Assert(ll.SelectOne);

+            if (!ContainsFreeVariable(ll.Seq, false, i)) {

+              Fi = ll.E0;

+              lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, ll.Seq, e, null); l.Type = ll.Type; return l; };

+            } else if (!ContainsFreeVariable(ll.E0, false, i)) {

+              Fi = ll.Seq;

+              lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, e, ll.E0, null); l.Type = ll.Type; return l; };

+            }

+          }

+        }

         var rhs = ((ExprRhs)s0.Rhs).Expr;

-        var g = prevEtran.TrExpr(rhs);

-        GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField);

-        var xHeapOF = ExpressionTranslator.ReadHeap(s.Tok, etran.HeapExpr, xObj, xField);

-

-        Type lhsType;

-        if (lhs is FieldSelectExpr) {

-          lhsType = ((FieldSelectExpr)lhs).Type;

-        } else {

-          lhsType = null;

+        bool usedInversion = false;

+        if (Fi != null) {

+          var j = new BoundVar(i.tok, i.Name + "#inv", Fi.Type);

+          var jj = Expression.CreateIdentExpr(j);

+          var jList = new List<BoundVar>() { j };

+          var vals = InvertExpression(i, j, s.Range, Fi);

+#if DEBUG_PRINT

+          Console.WriteLine("DEBUG: Trying to invert:");

+          Console.WriteLine("DEBUG:   " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi));

+          if (vals == null) {

+            Console.WriteLine("DEBUG: Can't");

+          } else {

+            Console.WriteLine("DEBUG: The inverse is the disjunction of the following:");

+            foreach (var val in vals) {

+              Console.WriteLine("DEBUG:   " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name);

+            }

+          }

+#endif

+          if (vals != null) {

+            foreach (var val in vals) {

+              qq = TrForall_NewValueAssumption(s.Tok, jList, val.Range, lhsBuilder(jj), Substitute(rhs, i, val.FInverse), true, etran, prevEtran);

+              updater.Add(new Bpl.AssumeCmd(s.Tok, qq));

+            }

+            usedInversion = true;

+          }

         }

-        g = CondApplyBox(rhs.tok, g, rhs.Type, lhsType);

+        if (!usedInversion) {

+          qq = TrForall_NewValueAssumption(s.Tok, s.BoundVars, s.Range, lhs, rhs, false, etran, prevEtran);

+          updater.Add(new Bpl.AssumeCmd(s.Tok, qq));

+        }

+      }

+    }

+

+    /// <summary>

+    /// Generate:

+    ///   assume (forall x,y :: Range(x,y)[$Heap:=oldHeap] ==>

+    ///                         $Heap[ Object(x,y)[$Heap:=oldHeap], Field(x,y)[$Heap:=oldHeap] ] == G[$Heap:=oldHeap] ));

+    /// where

+    ///   x,y           represent boundVars

+    ///   Object(x,y)   is the first part of lhs

+    ///   Field(x,y)    is the second part of lhs

+    ///   G             is rhs

+    /// If lhsAsTrigger is true, then use the LHS of the equality above as the trigger; otherwise, don't specify any trigger.

+    /// </summary>

+    private Bpl.Expr TrForall_NewValueAssumption(IToken tok, List<BoundVar> boundVars, Expression range, Expression lhs, Expression rhs, bool lhsAsTrigger, ExpressionTranslator etran, ExpressionTranslator prevEtran) {

+      Contract.Requires(tok != null);

+      Contract.Requires(boundVars != null);

+      Contract.Requires(range != null);

+      Contract.Requires(lhs != null);

+      Contract.Requires(rhs != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(prevEtran != null);

+

+      var xBvars = new List<Variable>();

+      Bpl.Expr xAnte = etran.TrBoundVariables(boundVars, xBvars);

+      xAnte = BplAnd(xAnte, prevEtran.TrExpr(range));

+      var g = prevEtran.TrExpr(rhs);

+      Bpl.Expr obj, field;

+      GetObjFieldDetails(lhs, prevEtran, out obj, out field);

+      var xHeapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, obj, field);

+

+      Type lhsType = lhs is FieldSelectExpr ? ((FieldSelectExpr)lhs).Type : null;

+      g = CondApplyBox(rhs.tok, g, rhs.Type, lhsType);

+

+      Trigger tr = lhsAsTrigger ? new Trigger(tok, true, new List<Bpl.Expr>() { xHeapOF }) : null;

+      return new Bpl.ForallExpr(tok, xBvars, tr, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g)));

+    }

+

+    class ForallStmtTranslationValues

+    {

+      public readonly Expression Range;

+      public readonly Expression FInverse;

+      public ForallStmtTranslationValues(Expression range, Expression fInverse) {

+        Contract.Requires(range != null);

+        Contract.Requires(fInverse != null);

+        Range = range;

+        FInverse = fInverse;

+      }

+      public ForallStmtTranslationValues Subst(IVariable j, Expression e, Translator translator) {

+        Contract.Requires(j != null);

+        Contract.Requires(e != null);

+        Contract.Requires(translator != null);

+        var substMap = new Dictionary<IVariable, Expression>();

+        substMap.Add(j, e);

+        var v = new ForallStmtTranslationValues(translator.Substitute(Range, null, substMap), translator.Substitute(FInverse, null, substMap));

+        return v;

+      }

+    }

 

-        qq = new Bpl.ForallExpr(s.Tok, xBvars, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g)));

-        updater.Add(new Bpl.AssumeCmd(s.Tok, qq));

+    /// <summary>

+    /// Find piecewise inverse of F under R.  More precisely, find lists of expressions P and F-1

+    /// such that

+    ///     R(i) && j == F(i)

+    /// holds iff the disjunction of the following predicates holds:

+    ///     P_0(j) && F-1_0(j) == i

+    ///     ...

+    ///     P_{n-1}(j) && F-1_{n-1}(j) == i

+    /// If no such disjunction is found, return null.

+    /// If such a disjunction is found, return for each disjunct:

+    ///     * The predicate P_k(j), which is an expression that may have free occurrences of j (but no free occurrences of i)

+    ///     * The expression F-1_k(j), which also may have free occurrences of j but not of i

+    /// </summary>

+    private List<ForallStmtTranslationValues> InvertExpression(BoundVar i, BoundVar j, Expression R, Expression F) {

+      Contract.Requires(i != null);

+      Contract.Requires(j != null);

+      Contract.Requires(R != null);

+      Contract.Requires(F != null);

+      var vals = new List<ForallStmtTranslationValues>(InvertExpressionIter(i, j, R, F));

+      if (vals.Count == 0) {

+        return null;

+      } else {

+        return vals;

+      }

+    }

+    /// <summary>

+    /// See InvertExpression.

+    /// </summary>

+    private IEnumerable<ForallStmtTranslationValues> InvertExpressionIter(BoundVar i, BoundVar j, Expression R, Expression F) {

+      Contract.Requires(i != null);

+      Contract.Requires(j != null);

+      Contract.Requires(R != null);

+      Contract.Requires(F != null);

+      F = F.Resolved;

+      if (!ContainsFreeVariable(F, false, i)) {

+        // We're looking at R(i) && j == K.

+        // We cannot invert j == K, but if we're lucky, R(i) contains a conjunct i==G.

+        Expression r = Expression.CreateBoolLiteral(R.tok, true);

+        Expression G = null;

+        foreach (var c in Expression.Conjuncts(R)) {

+          if (G == null && c is BinaryExpr) {

+            var bin = (BinaryExpr)c;

+            if (BinaryExpr.IsEqualityOp(bin.ResolvedOp)) {

+              var id = bin.E0.Resolved as IdentifierExpr;

+              if (id != null && id.Var == i) {

+                G = bin.E1;

+                continue;

+              }

+              id = bin.E1.Resolved as IdentifierExpr;

+              if (id != null && id.Var == i) {

+                G = bin.E0;

+                continue;

+              }

+            }

+          }

+          r = Expression.CreateAnd(r, c);

+        }

+        if (G != null) {

+          var jIsK = Expression.CreateEq(Expression.CreateIdentExpr(j), F, j.Type);

+          var rr = Substitute(r, i, G);

+          yield return new ForallStmtTranslationValues(Expression.CreateAnd(rr, jIsK), G);

+        }

+      } else if (F is IdentifierExpr) {

+        var e = (IdentifierExpr)F;

+        if (e.Var == i) {

+          // We're looking at R(i) && j == i, which is particularly easy to invert:  R(j) && j == i

+          var jj = Expression.CreateIdentExpr(j);

+          yield return new ForallStmtTranslationValues(Substitute(R, i, jj), jj);

+        }

+      } else if (F is BinaryExpr) {

+        var bin = (BinaryExpr)F;

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

+          if (!ContainsFreeVariable(bin.E1, false, i)) {

+            // We're looking at:  R(i) && j == f(i) + K.

+            // By a recursive call, we'll ask to invert:  R(i) && j' == f(i).

+            // For each P_0(j') && f-1_0(j') == i we get back, we yield:

+            // P_0(j - K) && f-1_0(j - K) == i

+            var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E1);

+            foreach (var val in InvertExpression(i, j, R, bin.E0)) {

+              yield return val.Subst(j, jMinusK, this);

+            }

+          } else if (!ContainsFreeVariable(bin.E0, false, i)) {

+            // We're looking at:  R(i) && j == K + f(i)

+            // Do as in previous case, but with operands reversed.

+            var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E0);

+            foreach (var val in InvertExpression(i, j, R, bin.E1)) {

+              yield return val.Subst(j, jMinusK, this);

+            }

+          }

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

+          if (!ContainsFreeVariable(bin.E1, false, i)) {

+            // We're looking at:  R(i) && j == f(i) - K

+            // Recurse on f(i) and then replace j := j + K

+            var jPlusK = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E1);

+            foreach (var val in InvertExpression(i, j, R, bin.E0)) {

+              yield return val.Subst(j, jPlusK, this);

+            }

+          } else if (!ContainsFreeVariable(bin.E0, false, i)) {

+            // We're looking at:  R(i) && j == K - f(i)

+            // Recurse on f(i) and then replace j := K - j

+            var kMinusJ = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E0);

+            foreach (var val in InvertExpression(i, j, R, bin.E1)) {

+              yield return val.Subst(j, kMinusJ, this);

+            }

+          }

+        }

+      } else if (F is ITEExpr) {

+        var ife = (ITEExpr)F;

+        // We're looking at R(i) && j == if A(i) then B(i) else C(i), which is equivalent to the disjunction of:

+        //   R(i) && A(i) && j == B(i)

+        //   R(i) && !A(i) && j == C(i)

+        // We recurse on each one, yielding the results

+        var r = Expression.CreateAnd(R, ife.Test);

+        var valsThen = InvertExpression(i, j, r, ife.Thn);

+        if (valsThen != null) {

+          r = Expression.CreateAnd(R, Expression.CreateNot(ife.tok, ife.Test));

+          var valsElse = InvertExpression(i, j, r, ife.Els);

+          if (valsElse != null) {

+            foreach (var val in valsThen) { yield return val; }

+            foreach (var val in valsElse) { yield return val; }

+          }

+        }

       }

     }

 

@@ -10437,6 +10675,18 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Returns an expression like "expr", but where free occurrences of "v" have been replaced by "e".

+    /// </summary>

+    public Expression Substitute(Expression expr, IVariable v, Expression e) {

+      Contract.Requires(expr != null);

+      Contract.Requires(v != null);

+      Contract.Requires(e != null);

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

+      var substMap = new Dictionary<IVariable, Expression>();

+      substMap.Add(v, e);

+      return Substitute(expr, null, substMap);

+    }

     public Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap, Dictionary<TypeParameter, Type>/*?*/ typeMap = null) {

       Contract.Requires(expr != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

diff --git a/Test/dafny0/Inverses.dfy b/Test/dafny0/Inverses.dfy
new file mode 100644
index 00000000..7995255a
--- /dev/null
+++ b/Test/dafny0/Inverses.dfy
@@ -0,0 +1,112 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This identity function is used to so that if the occurrence of i below

+// that is enclosed by Id gets chosen by the SMT solver as a trigger, then

+// Id will be part of that trigger.  This means that the quantifier will

+// not match, and thus the 'forall' statement will be useless and the method

+// will not verify.  If, however, the inverting functionality in Dafny

+// works properly, then the 'i' in the right-hand side of the forall assignments

+// below will not be chosen in any trigger, and then the methods should

+// verify.

+function method Id(x: int): int { x }

+

+method Copy<T>(a: array<T>) returns (r: array<T>)

+  requires a != null;

+  ensures fresh(r) && r.Length == a.Length && forall k :: 0 <= k < a.Length ==> r[k] == a[k];

+{

+  r := new T[a.Length];

+  forall i | 0 <= i < a.Length {

+    r[i] := a[Id(i)];

+  }

+}

+

+method ShiftLeftA<T>(a: array<T>, n: nat) returns (r: array<T>)

+  requires a != null && n <= a.Length;

+  ensures fresh(r) && r.Length == a.Length - n && forall k :: n <= k < a.Length ==> r[k - n] == a[k];

+{

+  r := new T[a.Length - n];

+  forall i | 0 <= i < a.Length - n {

+    r[i] := a[i + n];

+  }

+}

+

+method ShiftLeftB<T>(a: array<T>, n: nat) returns (r: array<T>)

+  requires a != null && n <= a.Length;

+  ensures fresh(r) && r.Length == a.Length - n && forall k :: 0 <= k < a.Length - n ==> r[k] == a[k + n];

+{

+  r := new T[a.Length - n];

+  forall i | n <= i < a.Length {

+    r[i - n] := a[Id(i)];

+  }

+}

+

+method ShiftLeftC<T>(a: array<T>, n: nat) returns (r: array<T>)

+  requires a != null && n <= a.Length;

+  ensures fresh(r) && r.Length == a.Length - n && forall k :: 0 <= k < a.Length - n ==> r[k] == a[k + n];

+{

+  r := new T[a.Length - n];

+  forall i | n <= i < a.Length {

+    r[i + 15 - n - 15] := a[Id(i)];

+  }

+}

+

+method Insert<T>(a: array<T>, p: nat, n: nat) returns (r: array<T>)

+  requires a != null && p <= a.Length;

+  ensures fresh(r) && r.Length == a.Length + n;

+  ensures forall k :: 0 <= k < p ==> r[k] == a[k];

+  ensures forall k :: p <= k < a.Length ==> r[k + n] == a[k];

+{

+  r := new T[a.Length + n];

+  forall i | 0 <= i < a.Length {

+    r[if i < p then i else i + n] := a[Id(i)];

+  }

+}

+

+method RotateA<T>(a: array<T>) returns (r: array<T>)

+  requires a != null;

+  ensures fresh(r) && r.Length == a.Length;

+  ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];

+{

+  r := new T[a.Length];

+  forall i | 0 <= i < a.Length {

+    r[(i + 1) % a.Length] := a[Id(i)];  // error: Dafny does not find an inverse for this one,

+                                        // which causes Z3 to pick Id(i) as the trigger, which

+                                        // causes the verification to fail.

+  }

+}

+

+method RotateB<T>(a: array<T>) returns (r: array<T>)

+  requires a != null;

+  ensures fresh(r) && r.Length == a.Length;

+  ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];

+{

+  r := new T[a.Length];

+  forall i | 0 <= i < a.Length {

+    r[if i + 1 == a.Length then 0 else i + 1] := a[Id(i)];  // error: Dafny does not find an inverse

+                                                            // for this one, so (like in RotateA),

+                                                            // the verification fails.

+  }

+}

+

+method RotateC<T>(a: array<T>) returns (r: array<T>)

+  requires a != null;

+  ensures fresh(r) && r.Length == a.Length;

+  ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];

+{

+  r := new T[a.Length];

+  forall i | 0 <= i < a.Length {

+    r[if i == a.Length - 1 then 0 else i + 1] := a[Id(i)];  // yes, Dafny can invert this one

+  }

+}

+

+method RotateD<T>(a: array<T>) returns (r: array<T>)

+  requires a != null;

+  ensures fresh(r) && r.Length == a.Length;

+  ensures forall k :: 0 <= k < a.Length ==> r[(k + 1) % a.Length] == a[k];

+{

+  r := new T[a.Length];

+  forall i | 0 <= i < a.Length {

+    r[if a.Length - 1 == i then 0 else i + 1] := a[Id(i)];  // yes, Dafny can invert this one

+  }

+}

diff --git a/Test/dafny0/Inverses.dfy.expect b/Test/dafny0/Inverses.dfy.expect
new file mode 100644
index 00000000..a04f21dc
--- /dev/null
+++ b/Test/dafny0/Inverses.dfy.expect
@@ -0,0 +1,12 @@
+Inverses.dfy(70,1): Error BP5003: A postcondition might not hold on this return path.

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

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

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Else

+

+Dafny program verifier finished with 17 verified, 2 errors

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index a9d36932..a4bdf0a0 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -56,6 +56,24 @@ class {:autocontracts} RingBuffer<T>
     Contents := Contents + [x];

   }

 

+  method ResizingEnqueue(x: T)

+    ensures Contents == old(Contents) + [x] && N >= old(N);

+  {

+    if data.Length == len {

+      var more := data.Length + 1;

+      var d := new T[data.Length + more];

+      forall i | 0 <= i < data.Length {

+        d[if i < start then i else i + more] := data[i];

+      }

+      N, data, start := N + more, d, if len == 0 then 0 else start + more;

+    }

+    var nextEmpty := if start + len < data.Length 

+                     then start + len else start + len - data.Length;

+    data[nextEmpty] := x;

+    len := len + 1;

+    Contents := Contents + [x];

+  }

+

   method Dequeue() returns (x: T)

     requires Contents != [];

     modifies Repr;

diff --git a/Test/vstte2012/RingBufferAuto.dfy.expect b/Test/vstte2012/RingBufferAuto.dfy.expect
index aeb37948..b06ff8fc 100644
--- a/Test/vstte2012/RingBufferAuto.dfy.expect
+++ b/Test/vstte2012/RingBufferAuto.dfy.expect
@@ -1,2 +1,2 @@
 

-Dafny program verifier finished with 13 verified, 0 errors

+Dafny program verifier finished with 15 verified, 0 errors