Changed ranking function for Seq, so that it's compatible with data types.

9 files changed, 219 insertions, 35 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index dd0a6671..5d0b647f 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -388,6 +388,20 @@ axiom (forall<T> s: Seq T, v: T, n: int ::
   { Seq#Drop(Seq#Build(s, v), n) }

     0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );

 

+function Seq#Rank<T>(Seq T): int;

+axiom (forall s: Seq BoxType, i: int ::

+  { DtRank($Unbox(Seq#Index(s, i)): DatatypeType) }

+  0 <= i && i < Seq#Length(s) ==> DtRank($Unbox(Seq#Index(s, i)): DatatypeType) < Seq#Rank(s) );

+axiom (forall<T> s: Seq T, i: int ::

+  { Seq#Rank(Seq#Drop(s, i)) }

+  0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s) );

+axiom (forall<T> s: Seq T, i: int ::

+  { Seq#Rank(Seq#Take(s, i)) }

+  0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s) );

+axiom (forall<T> s: Seq T, i: int, j: int ::

+  { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) }

+  0 <= i && i < j && j <= Seq#Length(s) ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s) );

+

 // Additional axioms about common things

 axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty();  // [][..0] == []

 axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty();  // [][0..] == []

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 1fa55d33..ba993caf 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -534,6 +534,13 @@ namespace Microsoft.Dafny {
               rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

               q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));

               sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));

+              // axiom (forall params, SeqRank(arg) < DtRank(#dt.ctor(params)));

+              CreateBoundVariables(ctor.Formals, out bvs, out args);

+              lhs = FunctionCall(ctor.tok, BuiltinFunction.SeqRank, null, args[i]);

+              rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

+              rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

+              q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Lt(lhs, rhs));

+              sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));              

             } else if (arg.Type is SetType) {

               // axiom (forall params, d: Datatype :: arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));

               // that is:

@@ -2122,7 +2129,7 @@ namespace Microsoft.Dafny {
                 es = Substitute(es, null, decrSubstMap);

                 decrCallee.Add(exprTran.TrExpr(es));

               }

-              return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, null, null, false, true);

+              return DecreasesCheck(decrToks, decrTypes, decrTypes, decrCallee, decrCaller, null, null, false, true);

             };

 

 #if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE

@@ -5904,7 +5911,7 @@ namespace Microsoft.Dafny {
           types.Add(cce.NonNull(e.Type));

           decrs.Add(etran.TrExpr(e));

         }

-        Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, initDecr, null, null, true, false);

+        Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, initDecr, null, null, true, false);

         invariants.Add(new Bpl.AssumeCmd(s.Tok, decrCheck));

       }

 

@@ -5940,7 +5947,7 @@ namespace Microsoft.Dafny {
           types.Add(cce.NonNull(e.Type));

           decrs.Add(etran.TrExpr(e));

         }

-        Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false);

+        Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, oldBfs, loopBodyBuilder, " at end of loop iteration", false, false);

         string msg;

         if (inferredDecreases) {

           msg = "cannot prove termination; try supplying a decreases clause for the loop";

@@ -6371,7 +6378,8 @@ namespace Microsoft.Dafny {
 

       int N = Math.Min(contextDecreases.Count, calleeDecreases.Count);

       List<IToken> toks = new List<IToken>();

-      List<Type> types = new List<Type>();

+      List<Type> types0 = new List<Type>();

+      List<Type> types1 = new List<Type>();

       List<Bpl.Expr> callee = new List<Bpl.Expr>();

       List<Bpl.Expr> caller = new List<Bpl.Expr>();

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

@@ -6382,12 +6390,13 @@ namespace Microsoft.Dafny {
           break;

         }

         toks.Add(tok);

-        types.Add(e0.Type);

+        types0.Add(e0.Type);

+        types1.Add(e1.Type);

         callee.Add(etranCurrent.TrExpr(e0));

         caller.Add(etranInitial.TrExpr(e1));

       }

       bool endsWithWinningTopComparison = N == contextDecreases.Count && N < calleeDecreases.Count;

-      Bpl.Expr decrExpr = DecreasesCheck(toks, types, callee, caller, builder, "", endsWithWinningTopComparison, false);

+      Bpl.Expr decrExpr = DecreasesCheck(toks, types0, types1, callee, caller, builder, "", endsWithWinningTopComparison, false);

       if (allowance != null) {

         decrExpr = Bpl.Expr.Or(allowance, decrExpr);

       }

@@ -6404,26 +6413,27 @@ namespace Microsoft.Dafny {
     /// ee0 represents the new values and ee1 represents old values.

     /// If builder is non-null, then the check '0 ATMOST decr' is generated to builder.

     /// </summary>

-    Bpl.Expr DecreasesCheck(List<IToken/*!*/>/*!*/ toks, List<Type/*!*/>/*!*/ types, List<Bpl.Expr/*!*/>/*!*/ ee0, List<Bpl.Expr/*!*/>/*!*/ ee1,

+    Bpl.Expr DecreasesCheck(List<IToken/*!*/>/*!*/ toks, List<Type/*!*/>/*!*/ types0, List<Type/*!*/>/*!*/ types1, List<Bpl.Expr/*!*/>/*!*/ ee0, List<Bpl.Expr/*!*/>/*!*/ ee1,

                             Bpl.StmtListBuilder builder, string suffixMsg, bool allowNoChange, bool includeLowerBound)

     {

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

-      Contract.Requires(cce.NonNullElements(types));

+      Contract.Requires(cce.NonNullElements(types0));

+      Contract.Requires(cce.NonNullElements(types1));

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

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

       Contract.Requires(predef != null);

-      Contract.Requires(types.Count == ee0.Count && ee0.Count == ee1.Count);

+      Contract.Requires(types0.Count == types1.Count && types0.Count == ee0.Count && ee0.Count == ee1.Count);

       Contract.Requires(builder == null || suffixMsg != null);

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

 

-      int N = types.Count;

+      int N = types0.Count;

 

       // compute eq and less for each component of the lexicographic pair

       List<Bpl.Expr> Eq = new List<Bpl.Expr>(N);

       List<Bpl.Expr> Less = new List<Bpl.Expr>(N);

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

         Bpl.Expr less, atmost, eq;

-        ComputeLessEq(toks[i], types[i], ee0[i], ee1[i], out less, out atmost, out eq, includeLowerBound);

+        ComputeLessEq(toks[i], types0[i], types1[i], ee0[i], ee1[i], out less, out atmost, out eq, includeLowerBound);

         Eq.Add(eq);

         Less.Add(allowNoChange ? atmost : less);

       }

@@ -6437,7 +6447,7 @@ namespace Microsoft.Dafny {
           for (int i = 0; i < k; i++) {

             prefixIsLess = Bpl.Expr.Or(prefixIsLess, Less[i]);

           }

-          if (types[k] is IntType) {

+          if (types0[k] is IntType) {

             Bpl.Expr bounded = Bpl.Expr.Le(Bpl.Expr.Literal(0), ee1[k]);

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

               bounded = Bpl.Expr.Or(bounded, Less[i]);

@@ -6474,9 +6484,9 @@ namespace Microsoft.Dafny {
       } else if (t is SetType) {

         return u is SetType;

       } else if (t is SeqType) {

-        return u is SeqType;

+        return u is SeqType || u.IsIndDatatype;

       } else if (t.IsDatatype) {

-        return u.IsDatatype;

+        return u.IsDatatype || (t.IsIndDatatype && u is SeqType);

       } else if (t.IsRefType) {

         return u.IsRefType;

       } else if (t is MultiSetType) {

@@ -6489,10 +6499,19 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void ComputeLessEq(IToken/*!*/ tok, Type/*!*/ ty, Bpl.Expr/*!*/ e0, Bpl.Expr/*!*/ e1, out Bpl.Expr/*!*/ less, out Bpl.Expr/*!*/ atmost, out Bpl.Expr/*!*/ eq, bool includeLowerBound)

+    Nullable<BuiltinFunction> RankFunction(Type/*!*/ ty)

+    {

+      Contract.Ensures(ty != null);

+      if (ty is SeqType)      return BuiltinFunction.SeqRank;

+      else if (ty.IsDatatype) return BuiltinFunction.DtRank;

+      else return null;

+    }

+

+    void ComputeLessEq(IToken/*!*/ tok, Type/*!*/ ty0, Type/*!*/ ty1, Bpl.Expr/*!*/ e0, Bpl.Expr/*!*/ e1, out Bpl.Expr/*!*/ less, out Bpl.Expr/*!*/ atmost, out Bpl.Expr/*!*/ eq, bool includeLowerBound)

      {

       Contract.Requires(tok != null);

-      Contract.Requires(ty != null);

+      Contract.Requires(ty0 != null);

+      Contract.Requires(ty1 != null);

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

       Contract.Requires(predef != null);

@@ -6500,20 +6519,29 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.ValueAtReturn(out atmost)!=null);

       Contract.Ensures(Contract.ValueAtReturn(out eq)!=null);

 

-      if (ty is BoolType) {

+      Nullable<BuiltinFunction> rk0 = RankFunction(ty0);

+      Nullable<BuiltinFunction> rk1 = RankFunction(ty1);

+      if (rk0 != null && rk1 != null && rk0 != rk1)

+      {

+        eq = Bpl.Expr.False;

+        Bpl.Expr b0 = FunctionCall(tok, rk0.Value, null, e0);

+        Bpl.Expr b1 = FunctionCall(tok, rk1.Value, null, e1);

+        less = Bpl.Expr.Lt(b0, b1);

+        atmost = Bpl.Expr.Le(b0, b1);

+      }

+      else if (ty0 is BoolType) {

         eq = Bpl.Expr.Iff(e0, e1);

         less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);

         atmost = Bpl.Expr.Imp(e0, e1);

-

-      } else if (ty is IntType || ty is SeqType || ty.IsDatatype) {

+      } else if (ty0 is IntType || ty0 is SeqType || ty0.IsDatatype) {

         Bpl.Expr b0, b1;

-        if (ty is IntType) {

+        if (ty0 is IntType) {

           b0 = e0;

           b1 = e1;

-        } else if (ty is SeqType) {

-          b0 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e0);

-          b1 = FunctionCall(tok, BuiltinFunction.SeqLength, null, e1);

-        } else if (ty.IsDatatype) {

+        } else if (ty0 is SeqType) {

+          b0 = FunctionCall(tok, BuiltinFunction.SeqRank, null, e0);

+          b1 = FunctionCall(tok, BuiltinFunction.SeqRank, null, e1);

+        } else if (ty0.IsDatatype) {

           b0 = FunctionCall(tok, BuiltinFunction.DtRank, null, e0);

           b1 = FunctionCall(tok, BuiltinFunction.DtRank, null, e1);

         } else {

@@ -6522,22 +6550,22 @@ namespace Microsoft.Dafny {
         eq = Bpl.Expr.Eq(b0, b1);

         less = Bpl.Expr.Lt(b0, b1);

         atmost = Bpl.Expr.Le(b0, b1);

-        if (ty is IntType && includeLowerBound) {

+        if (ty0 is IntType && includeLowerBound) {

           less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), less);

           atmost = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), b0), atmost);

         }

 

-      } else if (ty is EverIncreasingType) {

+      } else if (ty0 is EverIncreasingType) {

         eq = Bpl.Expr.Eq(e0, e1);

         less = Bpl.Expr.Gt(e0, e1);

         atmost = Bpl.Expr.Ge(e0, e1);

 

-      } else if (ty is SetType || ty is MapType) {

+      } else if (ty0 is SetType || ty0 is MapType) {

         Bpl.Expr b0, b1;

-        if (ty is SetType) {

+        if (ty0 is SetType) {

           b0 = e0;

           b1 = e1;

-        } else if (ty is MapType) {

+        } else if (ty0 is MapType) {

           // for maps, compare their domains as sets

           b0 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType(tok, predef.BoxType, predef.BoxType), e0);

           b1 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType(tok, predef.BoxType, predef.BoxType), e1);

@@ -6548,14 +6576,14 @@ namespace Microsoft.Dafny {
         less = ProperSubset(tok, b0, b1);

         atmost = FunctionCall(tok, BuiltinFunction.SetSubset, null, b0, b1);

 

-      } else if (ty is MultiSetType) {

+      } else if (ty0 is MultiSetType) {

         eq = FunctionCall(tok, BuiltinFunction.MultiSetEqual, null, e0, e1);

         less = ProperMultiset(tok, e0, e1);

         atmost = FunctionCall(tok, BuiltinFunction.MultiSetSubset, null, e0, e1);

 

       } else {

         // reference type

-        Contract.Assert(ty.IsRefType);  // otherwise, unexpected type

+        Contract.Assert(ty0.IsRefType);  // otherwise, unexpected type

         var b0 = Bpl.Expr.Neq(e0, predef.Null);

         var b1 = Bpl.Expr.Neq(e1, predef.Null);

         eq = Bpl.Expr.Iff(b0, b1);

@@ -8691,6 +8719,7 @@ namespace Microsoft.Dafny {
       SeqEqual,

       SeqSameUntil,

       SeqFromArray,

+      SeqRank,

 

       MapEmpty,

       MapCard,

@@ -8887,6 +8916,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 2);

           Contract.Assert(typeInstantiation != null);

           return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args);

+        case BuiltinFunction.SeqRank:

+          Contract.Assert(args.Length == 1);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "Seq#Rank", Bpl.Type.Int, args);

 

         case BuiltinFunction.MapEmpty: {

             Contract.Assert(args.Length == 0);

@@ -9366,7 +9399,7 @@ namespace Microsoft.Dafny {
           }

           Expression bodyK = Substitute(e.LogicalBody(), null, substMap);

 

-          Bpl.Expr less = DecreasesCheck(toks, types, kk, nn, null, null, false, true);

+          Bpl.Expr less = DecreasesCheck(toks, types, types, kk, nn, null, null, false, true);

 

           Bpl.Expr ihBody = etran.TrExpr(bodyK);

           if (!position) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index dd5e620f..97097cfd 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1671,6 +1671,30 @@ Execution trace:
 

 Dafny program verifier finished with 38 verified, 11 errors

 

+-------------------- RankPos.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

+

+-------------------- RankNeg.dfy --------------------

+RankNeg.dfy(7,26): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+RankNeg.dfy(12,28): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+RankNeg.dfy(19,31): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+RankNeg.dfy(29,25): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon5_Else

+    (0,0): anon6_Then

+

+Dafny program verifier finished with 1 verified, 4 errors

+

 -------------------- Superposition.dfy --------------------

 
 Verifying CheckWellformed$$_0_M0.C.M ...

diff --git a/Test/dafny0/RankNeg.dfy b/Test/dafny0/RankNeg.dfy
new file mode 100644
index 00000000..39e7630d
--- /dev/null
+++ b/Test/dafny0/RankNeg.dfy
@@ -0,0 +1,31 @@
+// Negative tests

+

+// Not well-founded mutual recursions.

+

+function seq_loop_i(xs: seq<int>): int

+{

+  if (xs == [1, 2]) then seq_loop_s([[1,2]])

+  else 0

+}

+function seq_loop_s(xs: seq<seq<int>>): int

+{

+  if (xs == [[1, 2]]) then seq_loop_i([1,2])

+  else 0

+}

+

+datatype wrap = X | WS(ds: seq<wrap>);

+function wrap_loop_1(xs: seq<wrap>): int

+{

+  if (xs == [WS([X,X])]) then wrap_loop_2(WS([X,X]))

+  else 0

+}

+function wrap_loop_2(xs: wrap): int

+{

+  if (xs == WS([X,X])) then wrap_loop_3([X,X])

+  else 0

+}

+function wrap_loop_3(xs: seq<wrap>): int

+{

+  if (xs == [X,X]) then wrap_loop_1([WS([X,X])])

+  else 0

+}

diff --git a/Test/dafny0/RankPos.dfy b/Test/dafny0/RankPos.dfy
new file mode 100644
index 00000000..bc48a6c8
--- /dev/null
+++ b/Test/dafny0/RankPos.dfy
@@ -0,0 +1,79 @@
+datatype list<A> = Nil | Cons(head: A, tail: list<A>);

+datatype d = A | B(ds: list<d>);

+datatype d2 = A2 | B2(ds: seq<d2>);

+datatype d3 = A3 | B3(ds: set<d3>);

+

+function d_size(x: d): int

+{

+  match x

+  case A => 1

+  case B(ds) => 1+ds_size(ds)

+}

+

+function ds_size(xs: list<d>): int

+{

+  match xs

+  case Nil => 1

+  case Cons(head, tail) => d_size(head)+ds_size(tail)

+}

+

+function d2_size(x: d2): int

+{

+  match x

+  case A2 => 1

+  case B2(ds) => 1+ds2_size(ds)

+}

+

+function ds2_size(xs: seq<d2>): int

+{

+  if (|xs|==0) then 1 else 1+d2_size(xs[0])+ds2_size(xs[1..])

+}

+

+function seq_dec_drop(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  1+seq_dec_drop(xs[1..])

+}

+

+function seq_dec_take(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  1+seq_dec_take(xs[..|xs|-1])

+}

+

+function seq_dec(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 < i <= |xs|;

+  i+seq_dec(xs[i..])

+}

+

+function seq_dec'(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 <= i < |xs|;

+  i+seq_dec'(xs[..i])

+}

+

+function seq_dec''(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 <= i < |xs|;

+  assert xs[0..i] == xs[..i];

+  i+seq_dec''(xs[0..i])

+}

+

+function seq_dec'''(xs: seq<int>): int

+  decreases |xs|;

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 <= i < |xs|;

+  i+seq_dec'''(xs[..i]+xs[i+1..])

+}

+

+function seq_dec''''(xs: seq<int>): int

+{

+  if (|xs|==0) then 0 else

+  var i :| 0 <= i < |xs|;

+  i+seq_dec''''(xs[..i]+xs[i+1..])

+}
\ No newline at end of file
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 1bb2ef9f..c238b1f4 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -25,7 +25,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy

             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

-            Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (

+            Calculations.dfy IteratorResolution.dfy Iterators.dfy

+            RankPos.dfy RankNeg.dfy) do (

   echo.

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

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index adf97863..57ac69c7 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -83,7 +83,7 @@ class ExtensibleArray<T> {
     modifies Repr;

     ensures Valid() && fresh(Repr - old(Repr));

     ensures Contents == old(Contents) + [t];

-    decreases Contents;

+    decreases |Contents|;

   {

     if (length == 0 || length % 256 != 0) {

       // there is room in "elements"

diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
index a3c5593c..b05af9f9 100644
--- a/Test/dafny1/ExtensibleArrayAuto.dfy
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -70,7 +70,7 @@ class {:autocontracts} ExtensibleArray<T> {
 

   method Append(t: T)

     ensures Contents == old(Contents) + [t];

-    decreases Contents;

+    decreases |Contents|;

   {

     if (length == 0 || length % 256 != 0) {

       // there is room in "elements"

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index f51a36b2..7ce48fcc 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -55,6 +55,8 @@ class {:autocontracts} RingBuffer<T>
 

   method Dequeue() returns (x: T)

     requires Contents != [];

+    modifies Repr;

+    ensures Valid() && fresh(Repr - old(Repr));

     ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);

   {

     x := data[start];