Dafny:

* Improved design and implementation of SplitExpr
* Fixed some tests in dafny0/Use.dfy
* Added test case (in dafny0/Termination.dfy) to test the recent strengthening of set axioms

6 files changed, 264 insertions, 124 deletions

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 1740bf8b..348fdd2b 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -1632,39 +1632,50 @@ namespace Microsoft.Dafny {
       if (!wellformednessProc) {

         string comment = "user-defined preconditions";

         foreach (MaybeFreeExpression p in m.Req) {

-          Bpl.RequiresSeq pieces = new Bpl.RequiresSeq();

-          if (!p.IsFree) {

-            foreach (Expression se in SplitExpr(p.E, true)) {

-              pieces.Add(Requires(se.tok, false, etran.TrExpr(se), null, null));

-            }

-          }

-          if (pieces.Length == 1) {

-            // add 1 checked precondition (the whole thing)

-            req.Add(Requires(p.E.tok, false, etran.TrExpr(p.E), null, comment));

-          } else {

-            // add 1 free precondition, followed by each piece (if any) as a checked precondition

+          if (p.IsFree) {

             req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));

-            req.AddRange(pieces);

+          } else {

+            List<Expression!>! definitions, pieces;

+            if (!SplitExpr(p.E, out definitions, out pieces)) {

+              req.Add(Requires(p.E.tok, false, etran.TrExpr(p.E), null, comment));

+            } else {

+              req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));  // add the entire condition as a free precondition

+              Bpl.Expr ante = Bpl.Expr.True;

+              foreach (Expression d in definitions) {

+                Bpl.Expr trD = etran.TrExpr(d);

+                req.Add(Requires(d.tok, true, trD, null, null));

+                ante = Bpl.Expr.And(ante, trD);

+              }

+              foreach (Expression se in pieces) {

+                req.Add(Requires(se.tok, false, Bpl.Expr.Imp(ante, etran.TrExpr(se)), null, null));  // TODO: it would be fine to have these use {:subsumption 0}

+              }

+            }

           }

           comment = null;

         }

         comment = "user-defined postconditions";

         foreach (MaybeFreeExpression p in m.Ens) {

-          Bpl.EnsuresSeq pieces = new Bpl.EnsuresSeq();

-          if (!p.IsFree) {

-            foreach (Expression se in SplitExpr(p.E, true)) {

-              pieces.Add(Ensures(se.tok, false, etran.TrExpr(se), null, null));

-            }

-          }

-          if (pieces.Length == 1) {

-            ens.Add(Ensures(p.E.tok, false, etran.TrExpr(p.E), null, comment));

-          } else {

+          if (p.IsFree) {

             ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));

-            ens.AddRange(pieces);

+          } else {

+            List<Expression!>! definitions, pieces;

+            if (!SplitExpr(p.E, out definitions, out pieces)) {

+              ens.Add(Ensures(p.E.tok, false, etran.TrExpr(p.E), null, comment));

+            } else {

+              ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));  // add the entire condition as a free postcondition

+              Bpl.Expr ante = Bpl.Expr.True;

+              foreach (Expression d in definitions) {

+                Bpl.Expr trD = etran.TrExpr(d);

+                ens.Add(Ensures(d.tok, true, trD, null, null));

+                ante = Bpl.Expr.And(ante, trD);

+              }

+              foreach (Expression se in pieces) {

+                ens.Add(Ensures(se.tok, false, Bpl.Expr.Imp(ante, etran.TrExpr(se)), null, null));  // TODO: it would be fine to have these use {:subsumption 0}

+              }

+            }

           }

           comment = null;

         }

-      

         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m, etran.Old, etran)) {

           ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));

         }

@@ -1865,12 +1876,16 @@ namespace Microsoft.Dafny {
         AddComment(builder, stmt, "assert statement");

         AssertStmt s = (AssertStmt)stmt;

         builder.Add(AssertNS(s.Expr.tok, IsTotal(s.Expr, etran), "assert condition must be well defined"));  // totality check

-        int pieces = 0;

-        foreach (Expression p in SplitExpr(s.Expr, true)) {

-          builder.Add(Assert(p.tok, etran.TrExpr(p), "assertion violation"));

-          pieces++;

-        }

-        if (2 <= pieces) {

+        List<Expression!>! definitions, pieces;

+        if (!SplitExpr(s.Expr, out definitions, out pieces)) {

+          builder.Add(Assert(s.Expr.tok, etran.TrExpr(s.Expr), "assertion violation"));

+        } else {

+          foreach (Expression p in definitions) {

+            builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));

+          }

+          foreach (Expression p in pieces) {

+            builder.Add(AssertNS(p.tok, etran.TrExpr(p), "assertion violation"));

+          }

           builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

         }

       } else if (stmt is AssumeStmt) {

@@ -2159,21 +2174,27 @@ namespace Microsoft.Dafny {
         List<Bpl.PredicateCmd!> invariants = new List<Bpl.PredicateCmd!>();

         Bpl.StmtListBuilder invDefinednessBuilder = new Bpl.StmtListBuilder();

         foreach (MaybeFreeExpression loopInv in s.Invariants) {

-          int pieces = 0;

+          invDefinednessBuilder.Add(AssertNS(loopInv.E.tok, IsTotal(loopInv.E, etran), (loopInv.IsFree ? "free " : "") + "loop invariant must be well defined"));  // totality check

+          invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));

           if (loopInv.IsFree) {

-            // still check the free invariant to be well defined

-            invDefinednessBuilder.Add(AssertNS(loopInv.E.tok, IsTotal(loopInv.E, etran), "free loop invariant must be well defined"));  // totality check

+            invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));

           } else {

-            invDefinednessBuilder.Add(AssertNS(loopInv.E.tok, IsTotal(loopInv.E, etran), "loop invariant must be well defined"));  // totality check

-            invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));

-            foreach (Expression se in SplitExpr(loopInv.E, true)) {

-              invariants.Add(Assert(se.tok, Bpl.Expr.Imp(w, etran.TrExpr(se)), "loop invariant violation"));

-              pieces++;

+            List<Expression!>! definitions, pieces;

+            if (!SplitExpr(loopInv.E, out definitions, out pieces)) {

+              invariants.Add(Assert(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E)), "loop invariant violation"));

+            } else {

+              Bpl.Expr ante = w;

+              foreach (Expression d in definitions) {

+                Bpl.Expr trD = etran.TrExpr(d);

+                invariants.Add(new Bpl.AssumeCmd(d.tok, trD));

+                ante = Bpl.Expr.And(ante, trD);

+              }

+              foreach (Expression se in pieces) {

+                invariants.Add(Assert(se.tok, Bpl.Expr.Imp(ante, etran.TrExpr(se)), "loop invariant violation"));  // TODO: it would be fine to have this use {:subsumption 0}

+              }

+              invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));

             }

           }

-          if (pieces != 1) {

-            invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));

-          }

         }

         // check definedness of decreases clause

         foreach (Expression e in theDecreases) {

@@ -2307,15 +2328,20 @@ namespace Microsoft.Dafny {
 

         // sequence of asserts and assumes and uses

         foreach (PredicateStmt ps in s.BodyPrefix) {

-          int pieces = 0;

           if (ps is AssertStmt) {

             Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(ps.Expr, etran)));

             builder.Add(AssertNS(ps.Expr.tok, q, "assert condition must be well defined"));  // totality check

-            foreach (Expression se in SplitExpr(ps.Expr, true)) {

+            List<Expression!>! definitions, pieces;

+            SplitExpr(ps.Expr, out definitions, out pieces);

+            foreach (Expression d in definitions) {

+              Bpl.Expr e = etran.TrExpr(d);

+              q = new Bpl.ForallExpr(d.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));

+              builder.Add(new Bpl.AssumeCmd(d.tok, q));

+            }

+            foreach (Expression se in pieces) {

               Bpl.Expr e = etran.TrExpr(se);

               q = new Bpl.ForallExpr(se.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));

-              builder.Add(Assert(se.tok, q, "assertion violation"));

-              pieces++;

+              builder.Add(Assert(se.tok, q, "assertion violation"));  // TODO: it would be a fine idea to let this use {:subsumption 0}

             }

           } else if (ps is AssumeStmt) {

             Bpl.Expr eIsTotal = IsTotal(ps.Expr, etran);

@@ -2325,17 +2351,15 @@ namespace Microsoft.Dafny {
             assert ps is UseStmt;

             // no totality check (see UseStmt case above)

           }

-          if (pieces != 1) {

-            Bpl.Expr e;

-            if (ps is UseStmt) {

-              UseStmt us = (UseStmt)ps;

-              e = (us.EvalInOld ? etran.Old : etran).TrUseExpr(us.FunctionCallExpr);

-            } else {

-              e = etran.TrExpr(ps.Expr);

-            }

-            Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));

-            builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, q));

+          Bpl.Expr enchilada;  // the whole enchilada

+          if (ps is UseStmt) {

+            UseStmt us = (UseStmt)ps;

+            enchilada = (us.EvalInOld ? etran.Old : etran).TrUseExpr(us.FunctionCallExpr);

+          } else {

+            enchilada = etran.TrExpr(ps.Expr);

           }

+          Bpl.Expr qEnchilada = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, enchilada));

+          builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, qEnchilada));

         }

 

         // Check RHS of assignment to be well defined

@@ -3657,67 +3681,86 @@ namespace Microsoft.Dafny {
       return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), aa);

     }

 

-    public IEnumerable<Expression!>! SplitExpr(Expression! expr, bool expandFunctions)

+    public bool SplitExpr(Expression! expr, out List<Expression!>! definitions, out List<Expression!>! pieces) {

+      definitions = new List<Expression!>();

+      pieces = new List<Expression!>();

+      return SplitExpr(expr, true, definitions, pieces);

+    }

+

+    ///<summary>

+    /// Returns false if no split occurred (in that case, nothing was added to definitions, and (exactly) expr itself was added to pieces.

+    ///</summary>

+    public bool SplitExpr(Expression! expr, bool expandFunctions, List<Expression!>! definitions, List<Expression!>! pieces)

       requires expr.Type is BoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type is BoolType);

     {

       if (expr is BoxingCastExpr) {

         BoxingCastExpr bce = (BoxingCastExpr)expr;

-        foreach (Expression e in SplitExpr(bce.E, expandFunctions)) {

-          assert bce != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one

-          Expression r = new BoxingCastExpr(e, bce.FromType, bce.ToType);

-          r.Type = bce.ToType;  // resolve here

-          yield return r;

+        List<Expression!> pp = new List<Expression!>();

+        if (SplitExpr(bce.E, expandFunctions, definitions, pp)) {

+          foreach (Expression e in pp) {

+            Expression r = new BoxingCastExpr(e, bce.FromType, bce.ToType);

+            r.Type = bce.ToType;  // resolve here

+            pieces.Add(r);

+          }

+          return true;

         }

         

       } else if (expr is BinaryExpr) {

         BinaryExpr bin = (BinaryExpr)expr;

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

-          foreach (Expression e in SplitExpr(bin.E0, expandFunctions)) {

-            yield return e;

-          }

-          assert bin != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one

-          foreach (Expression e in SplitExpr(bin.E1, expandFunctions)) {

-            yield return e;

-          }

-          yield break;

+          SplitExpr(bin.E0, expandFunctions, definitions, pieces);

+          SplitExpr(bin.E1, expandFunctions, definitions, pieces);

+          return true;

         

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

-          foreach (Expression e in SplitExpr(bin.E1, expandFunctions)) {

-            assert bin != null;

-            BinaryExpr redistributedExpr = new BinaryExpr(e.tok, bin.Op, bin.E0, e);

-            redistributedExpr.ResolvedOp = bin.ResolvedOp;  redistributedExpr.Type = bin.Type;  // resolve on the fly

-            yield return redistributedExpr;

+          List<Expression!> pp = new List<Expression!>();

+          if (SplitExpr(bin.E1, expandFunctions, definitions, pp)) {

+            foreach (Expression e in pp) {

+              BinaryExpr r = new BinaryExpr(e.tok, bin.Op, bin.E0, e);

+              r.ResolvedOp = bin.ResolvedOp;  r.Type = bin.Type;  // resolve on the fly

+              pieces.Add(r);

+            }

+            return true;

           }

-          yield break;

         }

       

       } else if (expr is ITEExpr) {

         ITEExpr ite = (ITEExpr)expr;

-        foreach (Expression e in SplitExpr(ite.Thn, expandFunctions)) {

-          assert ite != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one

-          BinaryExpr bin = new BinaryExpr(e.tok, BinaryExpr.Opcode.Imp, ite.Test, e);

-          bin.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  bin.Type = ite.Type;  // resolve on the fly

-          yield return bin;

+

+        List<Expression!> pp = new List<Expression!>();

+        SplitExpr(ite.Thn, expandFunctions, definitions, pp);

+        foreach (Expression e in pp) {

+          BinaryExpr r = new BinaryExpr(e.tok, BinaryExpr.Opcode.Imp, ite.Test, e);

+          r.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  r.Type = ite.Type;  // resolve on the fly

+          pieces.Add(r);

         }

-        assert ite != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one

+

         Expression negatedGuard = new UnaryExpr(ite.Test.tok, UnaryExpr.Opcode.Not, ite.Test);

         negatedGuard.Type = ite.Test.Type;  // resolve on the fly

-        foreach (Expression e in SplitExpr(ite.Els, expandFunctions)) {

-          assert ite != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one

-          assert negatedGuard != null;  // the necessity of this cast is a compiler bug, but perhaps an irrepairable one

-          BinaryExpr bin = new BinaryExpr(e.tok, BinaryExpr.Opcode.Imp, negatedGuard, e);

-          bin.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  bin.Type = ite.Type;  // resolve on the fly

-          yield return bin;

-        }

-        yield break;

+        pp = new List<Expression!>();

+        SplitExpr(ite.Els, expandFunctions, definitions, pp);

+        foreach (Expression e in pp) {

+          BinaryExpr r = new BinaryExpr(e.tok, BinaryExpr.Opcode.Imp, negatedGuard, e);

+          r.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  r.Type = ite.Type;  // resolve on the fly

+          pieces.Add(r);

+        }

+        return true;

       

       } else if (expr is OldExpr) {

-        foreach (Expression se in SplitExpr(((OldExpr)expr).E, expandFunctions)) {

-          OldExpr oe = new OldExpr(expr.tok, se);

-          oe.Type = se.Type;

-          yield return oe;

+        List<Expression!> dd = new List<Expression!>(), pp = new List<Expression!>();

+        if (SplitExpr(((OldExpr)expr).E, expandFunctions, dd, pp)) {

+          foreach (Expression e in dd) {

+            Expression r = new OldExpr(expr.tok, e);

+            r.Type = Type.Bool;  // resolve here

+            definitions.Add(r);

+          }

+          foreach (Expression e in pp) {

+            Expression r = new OldExpr(expr.tok, e);

+            r.Type = e.Type;  // resolve here

+            pieces.Add(r);

+          }

+          return true;

         }

-        yield break;

         

       } else if (expandFunctions && expr is FunctionCallExpr) {

         FunctionCallExpr fexp = (FunctionCallExpr)expr;

@@ -3734,18 +3777,28 @@ namespace Microsoft.Dafny {
             substMap.Add(p, arg);

           }

           Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap);

-          foreach (Expression se in SplitExpr(body, false)) {

-            assert fexp != null && fexp.Function != null;  // already checked above, but the compiler seems to have forgotten that

-            Expression piece = new UnboxingCastExpr(se, fexp.Function.ResultType, (!)expr.Type);

-            piece.Type = expr.Type;  // resolve here

-            yield return piece;

+

+          // add definition:  fn(args) ==> body

+          Expression bodyx = new UnboxingCastExpr(body, fexp.Function.ResultType, (!)expr.Type);

+          bodyx.Type = expr.Type;  // resolve here

+          BinaryExpr def = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Imp, fexp, bodyx);

+          def.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  def.Type = Type.Bool;  // resolve on the fly

+          definitions.Add(def);

+

+          // recurse on body

+          List<Expression!> pp = new List<Expression!>();

+          SplitExpr(body, false, definitions, pp);

+          foreach (Expression e in pp) {

+            Expression r = new UnboxingCastExpr(e, fexp.Function.ResultType, expr.Type);

+            r.Type = expr.Type;  // resolve here

+            pieces.Add(r);

           }

-          assert fexp != null && fexp.Function != null;  // already checked above, but the compiler seems to have forgotten that

-          yield break;

+          return true;

         }

       }

-      

-      yield return expr;

+

+      pieces.Add(expr); 

+      return false;

     }

     

     static Expression! Substitute(Expression! expr, Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7456ffaa..34b15b8a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -372,7 +372,7 @@ Execution trace:
     Termination.dfy(119,16): anon9_Else

     (0,0): anon5

 

-Dafny program verifier finished with 22 verified, 4 errors

+Dafny program verifier finished with 23 verified, 4 errors

 

 -------------------- Use.dfy --------------------

 Use.dfy(16,18): Error: assertion violation

@@ -393,17 +393,20 @@ Execution trace:
 Use.dfy(126,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(138,5): Error: assertion violation

+Use.dfy(143,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(138,5): Error: assertion violation

+Use.dfy(143,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(208,19): Error: assertion violation

+Use.dfy(143,5): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Use.dfy(213,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 39 verified, 9 errors

+Dafny program verifier finished with 39 verified, 10 errors

 

 -------------------- DTypes.dfy --------------------

 DTypes.dfy(15,14): Error: assertion violation

@@ -440,3 +443,7 @@ Dafny program verifier finished with 27 verified, 4 errors
 -------------------- Datatypes.dfy --------------------

 

 Dafny program verifier finished with 10 verified, 0 errors

+

+-------------------- SplitExpr.dfy --------------------

+

+Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny0/SplitExpr.dfy b/Test/dafny0/SplitExpr.dfy
new file mode 100644
index 00000000..80b67c10
--- /dev/null
+++ b/Test/dafny0/SplitExpr.dfy
@@ -0,0 +1,56 @@
+class UnboundedStack<T> {

+  var top: Node<T>;

+  ghost var footprint: set<object>;

+  ghost var content: seq<T>; 

+

+  function IsUnboundedStack(): bool

+    reads {this} + footprint;

+  {

+    this in footprint &&

+    (top == null  ==>  content == []) &&

+    (top != null  ==>  top in footprint && top.footprint <= footprint &&

+                       top.prev == null && content == top.content && top.Valid())

+  }

+

+  function IsEmpty(): bool

+    reads {this};

+  { content == [] }

+

+  method Pop() returns (result: T)

+    requires IsUnboundedStack() && !IsEmpty();

+    modifies footprint;

+    ensures IsUnboundedStack() && content == old(content)[1..];

+  {

+    result := top.val;

+    // The following assert does the trick, because it gets inlined and thus

+    // exposes top.next.Valid() (if top.next != null):

+    footprint := footprint - top.footprint;  top := top.next;

+    // In a previous version of the implementation of the SplitExpr transformation, the

+    // following assert did not have the intended effect of being used as a lemma:

+    assert top != null ==> top.Valid();

+    if (top != null) {

+      footprint := footprint + top.footprint;  top.prev := null;

+    }

+    content := content[1..];

+} }

+

+class Node<T> {

+  var val: T;  

+  var next: Node<T>;

+  var prev: Node<T>;

+  var footprint: set<Node<T>>;

+  var content: seq<T>;

+

+  function Valid(): bool

+    reads this, footprint;

+  {

+    this in footprint && !(null in footprint) &&

+    (next == null  ==>  content == [val])  &&

+    (next != null  ==>  next in footprint &&

+                        next.footprint < footprint &&

+                        !(this in next.footprint) &&

+                        next.prev == this &&

+                        content == [val] + next.content &&

+                        next.Valid())

+  }

+}

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 27004653..974dadab 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -151,3 +151,22 @@ method FailureToProveTermination5(b: bool, N: int)
     n := n + 1;

   }

 }

+

+class Node {

+  var next: Node;

+  var footprint: set<Node>;

+

+  function Valid(): bool

+    reads this, footprint;

+    // In a previous (and weaker) axiomatization of sets, there had been two problems

+    // with trying to prove the termination of this function.  First, the default

+    // decreases clause (derived from the reads clause) had been done incorrectly for

+    // a list of expressions.  Second, the set axiomatization had not been strong enough.

+  {

+    this in footprint && !(null in footprint) &&

+    (next != null  ==>  next in footprint &&

+                        next.footprint < footprint &&

+                        this !in next.footprint &&

+                        next.Valid())

+  }

+}

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 20928f41..7a963382 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -128,50 +128,55 @@ class T {
   }

 

   function K(): bool

-    reads this; decreases false;

+    reads this; decreases 0;

   {

-    x <= 100 || (1 < 0 && KK())

+    x <= 100 || (1 < 0 && KKK())

   }

-  unlimited function KK(): bool

-    reads this; decreases true;

+  function KK(): bool

+    reads this; decreases 1;

   {

     K()

   }

+  unlimited function KKK(): bool

+    reads this; decreases 2;

+  {

+    KK()

+  }

 

   method R0()

-    requires KK();

+    requires KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited

     modifies this;

   {

     x := x - 1;

-    assert KK();  // error (does not know exact definition of K from the initial state)

+    assert KKK();  // error (does not know exact definition of K from the initial state)

   }

 

   method R1()

-    requires KK();

+    requires KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited

     modifies this;

   {

-    use K();  // KK in the precondition and KK's definition give K#limited, which this use expands

+    use K();  // this equates K#limited and K, so the exact value of K() in the pre-state is now known

     x := x - 1;

-    assert KK();  // the assert expands KK to K, definition of K expands K

+    assert KKK();  // error: the assert expands KKK to KK, definition of KK expands K#limited (but not to K)

   }

 

   method R2()

-    requires KK();

+    requires KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited (but not K)

     modifies this;

   {

     x := x - 1;

-    use K();

-    assert KK();  // error (does not know exact definition of K in the pre-state)

+    use K();  // this equates K#limited and K in the present state

+    assert KKK();  // error: the connection with the pre-state K is not known

   }

 

   method R3()

-    requires KK();

+    requires KKK();  // this expands to both KKK() and KK(); the def. of KK() expands to K#limited (but not K)

     modifies this;

   {

-    use K();

+    use K();  // this equates K#limited and K, so the pre-state K() is known

     x := x - 1;

-    use K();

-    assert KK();  // thar it is

+    use K();  // this equates K#limited and K in the present state

+    assert KKK();  // thar it is:  this expands to both KKK and KK, and the def. of KK expands to K#limited

   }

 }

 

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index aa45ca05..0e8146c0 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -14,7 +14,7 @@ for %%f in (Simple.dfy) do (
 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

-            TypeParameters.dfy Datatypes.dfy) do (

+            TypeParameters.dfy Datatypes.dfy SplitExpr.dfy) do (

   echo.

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

   %DAFNY_EXE% /compile:0 %* %%f