Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic specifications

10 files changed, 631 insertions, 6 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 25627b7d..a5560d1c 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -111,6 +111,28 @@ namespace Microsoft.Dafny {
       return false;

     }

 

+    /// <summary>

+    /// Returns true if "nm" is a specified attribute.  If it is, then:

+    /// - if the attribute is {:nm true}, then value==true

+    /// - if the attribute is {:nm false}, then value==false

+    /// - if the attribute is anything else, then value returns as whatever it was passed in as.

+    /// </summary>

+    public static bool ContainsBool(Attributes attrs, string nm, ref bool value) {

+      Contract.Requires(nm != null);

+      for (; attrs != null; attrs = attrs.Prev) {

+        if (attrs.Name == nm) {

+          if (attrs.Args.Count == 1) {

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

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

+              value = (bool)arg.Value;

+            }

+          }

+          return true;

+        }

+      }

+      return false;

+    }

+

     public class Argument

     {

       public readonly IToken Tok;

@@ -1066,7 +1088,7 @@ namespace Microsoft.Dafny {
     public readonly List<FrameExpression/*!*/>/*!*/ Reads;

     public readonly List<Expression/*!*/>/*!*/ Ens;

     public readonly Specification<Expression>/*!*/ Decreases;

-    public readonly Expression Body;  // an extended expression

+    public Expression Body;  // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution

     public readonly bool SignatureIsOmitted;  // is "false" for all Function objects that survive into resolution

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -1133,7 +1155,7 @@ namespace Microsoft.Dafny {
     public readonly Specification<FrameExpression>/*!*/ Mod;

     public readonly List<MaybeFreeExpression/*!*/>/*!*/ Ens;

     public readonly Specification<Expression>/*!*/ Decreases;

-    public readonly BlockStmt Body;

+    public BlockStmt Body;  // Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -2683,6 +2705,88 @@ namespace Microsoft.Dafny {
     }

     public ResolvedOpcode ResolvedOp;  // filled in by resolution

 

+    public static Opcode ResolvedOp2SyntacticOp(ResolvedOpcode rop) {

+      switch (rop) {

+        case ResolvedOpcode.Iff: return Opcode.Iff;

+        case ResolvedOpcode.Imp: return Opcode.Imp;

+        case ResolvedOpcode.And: return Opcode.And;

+        case ResolvedOpcode.Or: return Opcode.Or;

+

+        case ResolvedOpcode.EqCommon:

+        case ResolvedOpcode.SetEq:

+        case ResolvedOpcode.MultiSetEq:

+        case ResolvedOpcode.SeqEq:

+          return Opcode.Eq;

+

+        case ResolvedOpcode.NeqCommon:

+        case ResolvedOpcode.SetNeq:

+        case ResolvedOpcode.MultiSetNeq:

+        case ResolvedOpcode.SeqNeq:

+          return Opcode.Neq;

+

+        case ResolvedOpcode.Lt:

+        case ResolvedOpcode.ProperSubset:

+        case ResolvedOpcode.ProperMultiSuperset:

+        case ResolvedOpcode.ProperPrefix:

+        case ResolvedOpcode.RankLt:

+          return Opcode.Lt;

+

+        case ResolvedOpcode.Le:

+        case ResolvedOpcode.Subset:

+        case ResolvedOpcode.MultiSubset:

+        case ResolvedOpcode.Prefix:

+          return Opcode.Le;

+

+        case ResolvedOpcode.Ge:

+        case ResolvedOpcode.Superset:

+        case ResolvedOpcode.MultiSuperset:

+          return Opcode.Ge;

+

+        case ResolvedOpcode.Gt:

+        case ResolvedOpcode.ProperSuperset:

+        case ResolvedOpcode.ProperMultiSubset:

+        case ResolvedOpcode.RankGt:

+          return Opcode.Gt;

+

+        case ResolvedOpcode.Add:

+        case ResolvedOpcode.Union:

+        case ResolvedOpcode.MultiSetUnion:

+        case ResolvedOpcode.Concat:

+          return Opcode.Add;

+

+        case ResolvedOpcode.Sub:

+        case ResolvedOpcode.SetDifference:

+        case ResolvedOpcode.MultiSetDifference:

+          return Opcode.Sub;

+

+        case ResolvedOpcode.Mul:

+        case ResolvedOpcode.Intersection:

+        case ResolvedOpcode.MultiSetIntersection:

+          return Opcode.Mul;

+

+        case ResolvedOpcode.Div: return Opcode.Div;

+        case ResolvedOpcode.Mod: return Opcode.Mod;

+

+        case ResolvedOpcode.Disjoint:

+        case ResolvedOpcode.MultiSetDisjoint:

+          return Opcode.Disjoint;

+

+        case ResolvedOpcode.InSet:

+        case ResolvedOpcode.InMultiSet:

+        case ResolvedOpcode.InSeq:

+          return Opcode.In;

+

+        case ResolvedOpcode.NotInSet:

+        case ResolvedOpcode.NotInMultiSet:

+        case ResolvedOpcode.NotInSeq:

+          return Opcode.NotIn;

+

+        default:

+          Contract.Assert(false);  // unexpected ResolvedOpcode

+          return Opcode.Add;  // please compiler

+      }

+    }

+

     public static string OpcodeString(Opcode op) {

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

 

diff --git a/Dafny/DafnyPipeline.csproj b/Dafny/DafnyPipeline.csproj
index 7264389b..cf2b51eb 100644
--- a/Dafny/DafnyPipeline.csproj
+++ b/Dafny/DafnyPipeline.csproj
@@ -158,6 +158,7 @@
     <Compile Include="Printer.cs" />

     <Compile Include="RefinementTransformer.cs" />

     <Compile Include="Resolver.cs" />

+    <Compile Include="Rewriter.cs" />

     <Compile Include="SccGraph.cs" />

     <Compile Include="Translator.cs" />

     <Compile Include="..\version.cs" />

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index f66a2c5c..3f3b23a0 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -170,9 +170,11 @@ namespace Microsoft.Dafny {
       }

 

       // register top-level declarations

+      Rewriter rewriter = new AutoContractsRewriter();

       var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls);

       var moduleNameInfo = new ModuleNameInformation[h];

       foreach (var m in mm) {

+        rewriter.PreResolve(m);

         if (m.RefinementBase != null) {

           var transformer = new RefinementTransformer(this);

           transformer.Construct(m);

@@ -193,6 +195,8 @@ namespace Microsoft.Dafny {
         // tear down

         classes = null;

         allDatatypeCtors = null;

+        // give rewriter a chance to do processing

+        rewriter.PostResolve(m);

       }

 

       // compute IsRecursive bit for mutually recursive functions

@@ -1733,8 +1737,7 @@ namespace Microsoft.Dafny {
           if (arrayRangeLhs == null && !sse.SelectOne) {

             arrayRangeLhs = sse;

           }

-        }

-        else {

+        } else {

           ResolveExpression(lhs, true);

         }

       }

diff --git a/Dafny/Rewriter.cs b/Dafny/Rewriter.cs
new file mode 100644
index 00000000..183337c2
--- /dev/null
+++ b/Dafny/Rewriter.cs
@@ -0,0 +1,319 @@
+using System;

+using System.Collections.Generic;

+using System.Diagnostics.Contracts;

+

+namespace Microsoft.Dafny

+{

+  public interface Rewriter

+  {

+    void PreResolve(ModuleDecl m);

+    void PostResolve(ModuleDecl m);

+  }

+

+  /// <summary>

+  /// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate

+  /// into a class.  From the user's perspective, what needs to be done is simply:

+  ///  - mark the class with {:autocontracts}

+  ///  - declare a function (or predicate) called Valid()

+  ///  

+  /// AutoContracts will then:

+  ///

+  /// Declare:

+  ///    ghost var Repr: set(object);

+  ///

+  /// For function/predicate Valid(), insert:

+  ///    reads this, Repr;

+  /// Into body of Valid(), insert (at the beginning of the body):

+  ///    this in Repr && null !in Repr

+  /// and also insert, for every array-valued field A declared in the class:

+  ///    (A != null ==> A in Repr) &&

+  /// and for every field F of a class type T where T has a field called Repr, also insert:

+  ///    (F != null ==> F in Repr && F.Repr SUBSET Repr && this !in Repr)

+  /// Except, if A or F is declared with {:autocontracts false}, then the implication will not

+  /// be added.

+  ///

+  /// For every constructor, add:

+  ///    modifies this;

+  ///    ensures Valid() && fresh(Repr - {this});

+  /// At the end of the body of the constructor, add:

+  ///    Repr := {this};

+  ///    if (A != null) { Repr := Repr + {A}; }

+  ///    if (F != null) { Repr := Repr + {F} + F.Repr; }

+  ///

+  /// For every method, add:

+  ///    requires Valid();

+  ///    modifies Repr;

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

+  /// At the end of the body of the method, add:

+  ///    if (A != null) { Repr := Repr + {A}; }

+  ///    if (F != null) { Repr := Repr + {F} + F.Repr; }

+  /// </summary>

+  public class AutoContractsRewriter : Rewriter

+  {

+    public void PreResolve(ModuleDecl m) {

+      foreach (var d in m.TopLevelDecls) {

+        bool sayYes = true;

+        if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) {

+          ProcessClassPreResolve((ClassDecl)d);

+        }

+      }

+    }

+

+    void ProcessClassPreResolve(ClassDecl cl) {

+      // Add:  ghost var Repr: set<object>;

+      // ...unless a field with that name is already present

+      if (!cl.Members.Exists(member => member is Field && member.Name == "Repr")) {

+        Type ty = new SetType(new ObjectType());

+        cl.Members.Add(new Field(cl.tok, "Repr", true, ty, null));

+      }

+

+      foreach (var member in cl.Members) {

+        bool sayYes = true;

+        if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {

+          continue;

+        }

+        var tok = member.tok;

+        if (member is Function && member.Name == "Valid" && !member.IsStatic) {

+          var valid = (Function)member;

+          // reads this;

+          valid.Reads.Add(new FrameExpression(new ThisExpr(tok), null));

+          // reads Repr;

+          valid.Reads.Add(new FrameExpression(new FieldSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"), null));

+        } else if (member is Constructor) {

+          var ctor = (Constructor)member;

+          // modifies this;

+          ctor.Mod.Expressions.Add(new FrameExpression(new ImplicitThisExpr(tok), null));

+          // ensures Valid();

+          ctor.Ens.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List<Expression>())));

+          // ensures fresh(Repr - {this});

+          var freshness = new FreshExpr(tok, new BinaryExpr(tok, BinaryExpr.Opcode.Sub,

+            new FieldSelectExpr(tok, new ImplicitThisExpr(tok), "Repr"),

+            new SetDisplayExpr(tok, new List<Expression>() { new ThisExpr(tok) })));

+          ctor.Ens.Insert(1, new MaybeFreeExpression(freshness));

+        } else if (member is Method && !member.IsStatic) {

+          var m = (Method)member;

+          // requires Valid();

+          m.Req.Insert(0, new MaybeFreeExpression(new FunctionCallExpr(tok, "Valid", new ImplicitThisExpr(tok), tok, new List<Expression>())));

+          // If this is a mutating method, we should also add a modifies clause and a postcondition, but we don't do that if it's

+          // a simple query method.  However, we won't know if it's a simple query method until after resolution, so we'll add the

+          // rest of the spec then.

+        }

+      }

+    }

+

+    public void PostResolve(ModuleDecl m) {

+      foreach (var d in m.TopLevelDecls) {

+        bool sayYes = true;

+        if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) {

+          ProcessClassPostResolve((ClassDecl)d);

+        }

+      }

+    }

+

+    void ProcessClassPostResolve(ClassDecl cl) {

+      // Find all fields of a reference type, and make a note of whether or not the reference type has a Repr field.

+      // Also, find the Repr field and the function Valid in class "cl"

+      Field ReprField = null;

+      Function Valid = null;

+      var subobjects = new List<Tuple<Field, Field>>();

+      foreach (var member in cl.Members) {

+        var field = member as Field;

+        if (field != null) {

+          bool sayYes = true;

+          if (field.Name == "Repr") {

+            ReprField = field;

+          } else if (Attributes.ContainsBool(field.Attributes, "autocontracts", ref sayYes) && !sayYes) {

+            // ignore this field

+          } else if (field.Type is ObjectType) {

+            subobjects.Add(new Tuple<Field, Field>(field, null));

+          } else if (field.Type.IsRefType) {

+            var rcl = (ClassDecl)((UserDefinedType)field.Type).ResolvedClass;

+            Field rRepr = null;

+            foreach (var memb in rcl.Members) {

+              var f = memb as Field;

+              if (f != null && f.Name == "Repr") {

+                rRepr = f;

+                break;

+              }

+            }

+            subobjects.Add(new Tuple<Field, Field>(field, rRepr));

+          }

+        } else if (member is Function && member.Name == "Valid" && !member.IsStatic) {

+          var fn = (Function)member;

+          if (fn.Formals.Count == 0 && fn.ResultType is BoolType) {

+            Valid = fn;

+          }

+        }

+      }

+      Contract.Assert(ReprField != null);  // we expect there to be a "Repr" field, since we added one in PreResolve

+

+      Type ty = new UserDefinedType(cl.tok, cl.Name, cl, new List<Type>());

+      var self = new ThisExpr(cl.tok);

+      self.Type = ty;

+      var implicitSelf = new ImplicitThisExpr(cl.tok);

+      implicitSelf.Type = ty;

+      var Repr = new FieldSelectExpr(cl.tok, implicitSelf, "Repr");

+      Repr.Field = ReprField;

+      Repr.Type = ReprField.Type;

+      var cNull = new LiteralExpr(cl.tok);

+      cNull.Type = new ObjectType();

+

+      foreach (var member in cl.Members) {

+        bool sayYes = true;

+        if (Attributes.ContainsBool(member.Attributes, "autocontracts", ref sayYes) && !sayYes) {

+          continue;

+        }

+        var tok = member.tok;

+        if (member is Function && member.Name == "Valid" && !member.IsStatic) {

+          var valid = (Function)member;

+          if (valid.IsGhost && valid.ResultType is BoolType) {

+            var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr);  // this in Repr

+            var c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, cNull, Repr);  // null !in Repr

+            var c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c0, c1);

+

+            foreach (var ff in subobjects) {

+              var F = new FieldSelectExpr(tok, implicitSelf, ff.Item1.Name);

+              F.Field = ff.Item1;

+              F.Type = ff.Item1.Type;

+

+              c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);

+              c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, F, Repr);

+              if (ff.Item2 == null) {

+                // F != null ==> F in Repr  (so, nothing else to do)

+              } else {

+                // F != null ==> F in Repr && F.Repr <= Repr && this !in F.Repr

+                var FRepr = new FieldSelectExpr(tok, F, ff.Item2.Name);

+                FRepr.Field = ff.Item2;

+                FRepr.Type = ff.Item2.Type;

+                var c2 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.Subset, FRepr, Repr);

+                var c3 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NotInSet, self, FRepr);

+                c1 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c1, BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c2, c3));

+              }

+              c = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c, BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.Imp, c0, c1));

+            }

+

+            if (valid.Body == null) {

+              valid.Body = c;

+            } else {

+              valid.Body = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, c, valid.Body);

+            }

+          }

+

+        } else if (member is Constructor) {

+          var ctor = (Constructor)member;

+          if (ctor.Body == null) {

+            ctor.Body = new BlockStmt(tok, new List<Statement>());

+          }

+          // TODO: these assignments should be included on every return path

+          var bodyStatements = ((BlockStmt)ctor.Body).Body;

+          // Repr := {this};

+          var e = new SetDisplayExpr(tok, new List<Expression>() { self });

+          e.Type = new SetType(new ObjectType());

+          Statement s = new AssignStmt(tok, Repr, new ExprRhs(e));

+          s.IsGhost = true;

+          bodyStatements.Add(s);

+

+          AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);

+

+        } else if (member is Method && !member.IsStatic) {

+          var m = (Method)member;

+          if (Valid != null && !IsSimpleQueryMethod(m)) {

+            // modifies Repr;

+            m.Mod.Expressions.Add(new FrameExpression(Repr, null));

+            // ensures Valid();

+            var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());

+            valid.Function = Valid;

+            valid.Type = Type.Bool;

+            m.Ens.Insert(0, new MaybeFreeExpression(valid));

+            // ensures fresh(Repr - old(Repr));

+            var e0 = new OldExpr(tok, Repr);

+            e0.Type = Repr.Type;

+            var e1 = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, Repr, e0);

+            e1.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference;

+            e1.Type = Repr.Type;

+            var freshness = new FreshExpr(tok, e1);

+            freshness.Type = Type.Bool;

+            m.Ens.Insert(1, new MaybeFreeExpression(freshness));

+

+            if (m.Body == null) {

+              m.Body = new BlockStmt(tok, new List<Statement>());

+            }

+            // TODO: these assignments should be included on every return path

+            var bodyStatements = ((BlockStmt)m.Body).Body;

+            AddSubobjectReprs(tok, subobjects, bodyStatements, self, implicitSelf, cNull, Repr);

+          }

+        }

+      }

+    }

+

+    void AddSubobjectReprs(Boogie.IToken tok, List<Tuple<Field, Field>> subobjects, List<Statement> bodyStatements,

+      Expression self, Expression implicitSelf, Expression cNull, Expression Repr) {

+

+      foreach (var ff in subobjects) {

+        var F = new FieldSelectExpr(tok, implicitSelf, ff.Item1.Name);

+        F.Field = ff.Item1;

+        F.Type = ff.Item1.Type;

+

+        Expression e = new SetDisplayExpr(tok, new List<Expression>() { F });

+        e.Type = new SetType(new ObjectType());

+        var rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, Repr, e);

+        rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;

+        rhs.Type = Repr.Type;

+        if (ff.Item2 == null) {

+          // Repr := Repr + {F}  (so, nothing else to do)

+        } else {

+          // Repr := Repr + {F} + F.Repr

+          var FRepr = new FieldSelectExpr(tok, F, ff.Item2.Name);

+          FRepr.Field = ff.Item2;

+          FRepr.Type = ff.Item2.Type;

+          rhs = new BinaryExpr(tok, BinaryExpr.Opcode.Add, rhs, FRepr);

+          rhs.ResolvedOp = BinaryExpr.ResolvedOpcode.Union;

+          rhs.Type = Repr.Type;

+        }

+        // Repr := Repr + ...;

+        Statement s = new AssignStmt(tok, Repr, new ExprRhs(rhs));

+        s.IsGhost = true;

+        // wrap if statement around s

+        e = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.NeqCommon, F, cNull);

+        var thn = new BlockStmt(tok, new List<Statement>() { s });

+        thn.IsGhost = true;

+        s = new IfStmt(tok, e, thn, null);

+        s.IsGhost = true;

+        // finally, add s to the body

+        bodyStatements.Add(s);

+      }

+    }

+

+    bool IsSimpleQueryMethod(Method m) {

+      // A simple query method has out parameters and its body has no effect other than to assign to them

+      return m.Outs.Count != 0 && m.Body != null && LocalAssignsOnly(m.Body);

+    }

+

+    bool LocalAssignsOnly(Statement s) {

+      Contract.Requires(s != null);

+      if (s is AssignStmt) {

+        var ss = (AssignStmt)s;

+        return ss.Lhs.Resolved is IdentifierExpr;

+      } else if (s is UpdateStmt) {

+        var ss = (UpdateStmt)s;

+        return ss.Lhss.TrueForAll(e => e.Resolved is IdentifierExpr);

+      } else if (s is CallStmt) {

+        return false;

+      } else {

+        foreach (var ss in s.SubStatements) {

+          if (!LocalAssignsOnly(ss)) {

+            return false;

+          }

+        }

+      }

+      return true;

+    }

+

+    BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {

+      var p = new BinaryExpr(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1);

+      p.ResolvedOp = rop;

+      p.Type = Type.Bool;

+      return p;

+    }

+  }

+}

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index ab10d944..023d80df 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -15,6 +15,10 @@ Dafny program verifier finished with 24 verified, 0 errors
 

 Dafny program verifier finished with 11 verified, 0 errors

 

+-------------------- ExtensibleArrayAuto.dfy --------------------

+

+Dafny program verifier finished with 11 verified, 0 errors

+

 -------------------- BinaryTree.dfy --------------------

 

 Dafny program verifier finished with 24 verified, 0 errors

diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
new file mode 100644
index 00000000..f7f97deb
--- /dev/null
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -0,0 +1,113 @@
+class {:autocontracts} ExtensibleArray<T> {

+  ghost var Contents: seq<T>;

+

+  var elements: array<T>;

+  var more: ExtensibleArray<array<T>>;

+  var length: int;

+  var M: int;  // shorthand for:  if more == null then 0 else 256 * |more.Contents|

+

+  function Valid(): bool

+  {

+    // shape of data structure

+    elements != null && elements.Length == 256 &&

+    (more != null ==>

+        elements !in more.Repr &&

+        more.Valid() &&

+        |more.Contents| != 0 &&

+        forall j :: 0 <= j && j < |more.Contents| ==>

+            more.Contents[j] != null && more.Contents[j].Length == 256 &&

+            more.Contents[j] in Repr && more.Contents[j] !in more.Repr &&

+            more.Contents[j] != elements &&

+            forall k :: 0 <= k && k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&

+

+    // length

+    M == (if more == null then 0 else 256 * |more.Contents|) &&

+    0 <= length && length <= M + 256 &&

+    (more != null ==> M < length) &&

+

+    // Contents

+    length == |Contents| &&

+    (forall i :: 0 <= i && i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&

+    (forall i :: M <= i && i < length ==> Contents[i] == elements[i - M])

+  }

+

+  constructor Init()

+    ensures Contents == [];

+  {

+    elements := new T[256];

+    more := null;

+    length := 0;

+    M := 0;

+    

+    Contents := [];

+  }

+

+  method Get(i: int) returns (t: T)

+    requires 0 <= i && i < |Contents|;

+    ensures t == Contents[i];

+    decreases Repr;

+  {

+    if (M <= i) {

+      t := elements[i - M];

+    } else {

+      var arr := more.Get(i / 256);

+      t := arr[i % 256];

+    }

+  }

+

+  method Set(i: int, t: T)

+    requires 0 <= i && i < |Contents|;

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

+  {

+    if (M <= i) {

+      elements[i - M] := t;

+    } else {

+      var arr := more.Get(i / 256);

+      arr[i % 256] := t;

+    }

+    Contents := Contents[i := t];

+  }

+

+  method Append(t: T)

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

+    decreases Repr;

+  {

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

+      // there is room in "elements"

+      elements[length - M] := t;

+    } else {

+      if (more == null) {

+        more := new ExtensibleArray<array<T>>.Init();

+        Repr := Repr + {more} + more.Repr;

+      }

+      // "elements" is full, so move it into "more" and allocate a new array

+      more.Append(elements);

+      Repr := Repr + more.Repr;

+      M := M + 256;

+      elements := new T[256];

+      Repr := Repr + {elements};

+      elements[0] := t;

+    }

+    length := length + 1;

+    Contents := Contents + [t];

+  }

+}

+

+method Main() {

+  var a := new ExtensibleArray<int>.Init();

+  var n := 0;

+  while (n < 256*256+600)

+    invariant a.Valid() && fresh(a.Repr);

+    invariant |a.Contents| == n;

+  {

+    a.Append(n);

+    n := n + 1;

+  }

+  var k := a.Get(570); print k, "\n";

+  k := a.Get(0); print k, "\n";

+  k := a.Get(1000); print k, "\n";

+  a.Set(1000, 23);

+  k := a.Get(0); print k, "\n";

+  k := a.Get(1000); print k, "\n";

+  k := a.Get(66000); print k, "\n";

+}

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 524765cf..0ad75ffa 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -12,7 +12,8 @@ for %%f in (BQueue.bpl) do (
   %BPLEXE% %* %%f

 )

 

-for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy

+for %%f in (Queue.dfy PriorityQueue.dfy

+            ExtensibleArray.dfy ExtensibleArrayAuto.dfy

             BinaryTree.dfy

             UnboundedStack.dfy

             SeparationLogicList.dfy

diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer
index 15a95de1..bca270c3 100644
--- a/Test/vstte2012/Answer
+++ b/Test/vstte2012/Answer
@@ -11,6 +11,10 @@ Dafny program verifier finished with 25 verified, 0 errors
 

 Dafny program verifier finished with 13 verified, 0 errors

 

+-------------------- RingBufferAuto.dfy --------------------

+

+Dafny program verifier finished with 13 verified, 0 errors

+

 -------------------- Tree.dfy --------------------

 

 Dafny program verifier finished with 15 verified, 0 errors

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
new file mode 100644
index 00000000..49f76713
--- /dev/null
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -0,0 +1,76 @@
+class {:autocontracts} RingBuffer<T>

+{

+  // public fields that are used to define the abstraction:

+  ghost var Contents: seq<T>;  // the contents of the ring buffer

+  ghost var N: nat;  // the capacity of the ring buffer

+

+  // Valid encodes the consistency of RingBuffer objects (think, invariant).

+  // An explanation of this idiom is explained in the README file.

+  predicate Valid

+  {

+    data != null &&

+    data.Length == N &&

+    (N == 0 ==> len == first == 0 && Contents == []) &&

+    (N != 0 ==> len <= N && first < N) &&

+    Contents == if first + len <= N then data[first..first+len] 

+                                    else data[first..] + data[..first+len-N]

+  }

+

+  // private implementation:

+  var data: array<T>;

+  var first: nat;

+  var len: nat;

+

+  constructor Create(n: nat)

+    ensures Contents == [] && N == n;

+  {

+    data := new T[n];

+    first, len := 0, 0;

+    Contents, N := [], n;

+  }

+

+  method Clear()

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

+  {

+    len := 0;

+    Contents := [];

+  }

+

+  method Head() returns (x: T)

+    requires Contents != [];

+    ensures x == Contents[0];

+  {

+    x := data[first];

+  }

+

+  method Push(x: T)

+    requires |Contents| != N;

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

+  {

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

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

+    data[nextEmpty] := x;

+    len := len + 1;

+    Contents := Contents + [x];

+  }

+

+  method Pop() returns (x: T)

+    requires Contents != [];

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

+  {

+    x := data[first];

+    first, len := if first + 1 == data.Length then 0 else first + 1, len - 1;

+    Contents := Contents[1..];

+  }

+}

+

+method TestHarness(x: int, y: int, z: int)

+{

+  var b := new RingBuffer<int>.Create(2);

+  b.Push(x);

+  b.Push(y);

+  var h := b.Pop();  assert h == x;

+  b.Push(z);

+  h := b.Pop();  assert h == y;

+  h := b.Pop();  assert h == z;

+}

diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 5145cb56..770f41dc 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -8,7 +8,7 @@ set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
 for %%f in (

     Two-Way-Sort.dfy

     Combinators.dfy

-    RingBuffer.dfy

+    RingBuffer.dfy RingBufferAuto.dfy

     Tree.dfy

     BreadthFirstSearch.dfy

   ) do (