Added Equals method on Type

Fixed some precondition violations
Various improvements in Contracts

8 files changed, 74 insertions, 14 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index d5bf1ecf..60084fb8 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -54,6 +54,7 @@ namespace Microsoft.Dafny {
 

     readonly int IndentAmount = 2;

     void Indent(int ind) {

+      Contract.Requires(0 <= ind);

       string spaces = "          ";

       for (; spaces.Length < ind; ind -= spaces.Length) {

         wr.Write(spaces);

@@ -61,7 +62,8 @@ namespace Microsoft.Dafny {
       wr.Write(spaces.Substring(0, ind));

     }

 

-    public void Compile(Program program) {Contract.Requires(program != null);

+    public void Compile(Program program) {

+      Contract.Requires(program != null);

       wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);

       wr.WriteLine();

       ReadRuntimeSystem();

@@ -757,6 +759,7 @@ namespace Microsoft.Dafny {
     }

 

     void CompileReturnBody(Expression body, int indent) {

+      Contract.Requires(0 <= indent);

       body = body.Resolved;

       if (body is MatchExpr) {

         MatchExpr me = (MatchExpr)body;

@@ -1693,6 +1696,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(sourceType != null);

       Contract.Requires(ctor != null);

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

+      Contract.Requires(0 <= indent);

       // if (source.is_Ctor0) {

       //   FormalType f0 = ((Dt_Ctor0)source._D).a0;

       //   ...

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b4724d0c..1b9408a8 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -212,6 +212,8 @@ namespace Microsoft.Dafny {
       }

     }

 

+    public abstract bool Equals(Type that);

+

     public bool IsSubrangeType {

       get { return this is NatType; }

     }

@@ -321,6 +323,9 @@ namespace Microsoft.Dafny {
     public override string TypeName(ModuleDefinition context) {

       return "bool";

     }

+    public override bool Equals(Type that) {

+      return that.Normalize() is BoolType;

+    }

   }

 

   public class IntType : BasicType {

@@ -328,6 +333,9 @@ namespace Microsoft.Dafny {
     public override string TypeName(ModuleDefinition context) {

       return "int";

     }

+    public override bool Equals(Type that) {

+      return that.Normalize() is IntType;

+    }

   }

 

   public class NatType : IntType

@@ -344,6 +352,9 @@ namespace Microsoft.Dafny {
     public override string TypeName(ModuleDefinition context) {

       return "object";

     }

+    public override bool Equals(Type that) {

+      return that.Normalize() is ObjectType;

+    }

   }

 

   public abstract class CollectionType : NonProxyType

@@ -373,6 +384,10 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<string>() != null);

       return "set<" + base.Arg.TypeName(context) + ">";

     }

+    public override bool Equals(Type that) {

+      var t = that.Normalize() as SetType;

+      return t != null && Arg.Equals(t.Arg);

+    }

   }

 

   public class MultiSetType : CollectionType

@@ -385,6 +400,10 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<string>() != null);

       return "multiset<" + base.Arg.TypeName(context) + ">";

     }

+    public override bool Equals(Type that) {

+      var t = that.Normalize() as MultiSetType;

+      return t != null && Arg.Equals(t.Arg);

+    }

   }

 

   public class SeqType : CollectionType {

@@ -397,6 +416,10 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<string>() != null);

       return "seq<" + base.Arg.TypeName(context) + ">";

     }

+    public override bool Equals(Type that) {

+      var t = that.Normalize() as SeqType;

+      return t != null && Arg.Equals(t.Arg);

+    }

   }

   public class MapType : CollectionType

   {

@@ -413,6 +436,10 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<string>() != null);

       return "map<" + Domain.TypeName(context) + ", " + Range.TypeName(context) + ">";

     }

+    public override bool Equals(Type that) {

+      var t = that.Normalize() as MapType;

+      return t != null && Arg.Equals(t.Arg);

+    }

   }

 

   public class UserDefinedType : NonProxyType

@@ -520,6 +547,11 @@ namespace Microsoft.Dafny {
       this.Path = new List<IToken>();

     }

 

+    public override bool Equals(Type that) {

+      var t = that.Normalize() as UserDefinedType;

+      return t != null && ResolvedClass == t.ResolvedClass && ResolvedParam == t.ResolvedParam;

+    }

+

     /// <summary>

     /// If type denotes a resolved class type, then return that class type.

     /// Otherwise, return null.

@@ -617,6 +649,15 @@ namespace Microsoft.Dafny {
         }

       }

     }

+    public override bool Equals(Type that) {

+      var i = Normalize();

+      if (i is TypeProxy) {

+        var u = that.Normalize() as TypeProxy;

+        return u != null && object.ReferenceEquals(i, u);

+      } else {

+        return i.Equals(that);

+      }

+    }

   }

 

   public abstract class UnrestrictedTypeProxy : TypeProxy {

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index d3847f10..726b0e99 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -338,7 +338,8 @@ namespace Microsoft.Dafny {
     const int IndentAmount = 2; // The amount of indent for each new scope

     const string BunchaSpaces = "                                ";

     void Indent(int amount)

-    {  Contract.Requires( 0 <= amount);

+    {

+      Contract.Requires(0 <= amount);

 

       while (0 < amount) {

         wr.Write(BunchaSpaces.Substring(0, amount));

@@ -807,6 +808,7 @@ namespace Microsoft.Dafny {
     }

 

     void PrintWhileStatement(int indent, WhileStmt s, bool omitGuard, bool omitBody) {

+      Contract.Requires(0 <= indent);

       if (omitGuard) {

         wr.WriteLine("while ...");

       } else {

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index e1070dad..a49b3b42 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -462,6 +462,7 @@ namespace Microsoft.Dafny
       moduleUnderConstruction = null;

     }

     Function CloneFunction(IToken tok, Function f, bool isGhost, List<Expression> moreEnsures, Expression moreBody, Expression replacementBody, bool checkPrevPostconditions, Attributes moreAttributes) {

+      Contract.Requires(tok != null);

       Contract.Requires(moreBody == null || f is Predicate);

       Contract.Requires(moreBody == null || replacementBody == null);

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 15652c60..2d847b1e 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -421,6 +421,8 @@ namespace Microsoft.Dafny
     }

 

     private string ModuleNotFoundErrorMessage(int i, List<IToken> path) {

+      Contract.Requires(path != null);

+      Contract.Requires(0 <= i && i < path.Count);

       return "module " + path[i].val + " does not exist" +

         (1 < path.Count ? " (position " + i.ToString() + " in path " + Util.Comma(".", path, x => x.val) + ")" : "");

     }

@@ -4768,6 +4770,8 @@ namespace Microsoft.Dafny
     /// "twoState" implies that "old" and "fresh" expressions are allowed.

     /// </summary>

     void ResolveExpression(Expression expr, bool twoState, ICodeContext codeContext) {

+      Contract.Requires(expr != null);

+      Contract.Requires(codeContext != null);

       ResolveExpression(expr, twoState, codeContext, null);

     }

 

@@ -5954,7 +5958,7 @@ namespace Microsoft.Dafny
       //  - static function or method of sig.

       // This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but

       // should not consult the local scope. This distingushes this from the above, in that local scope, imported modules, etc. are ignored.

-      Contract.Requires(p < e.Tokens.Count);

+      Contract.Requires(0 <= p && p < e.Tokens.Count);

       Expression r = null;  // resolved version of e

       CallRhs call = null;

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a6d5c2e9..f0d882af 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -139,6 +139,8 @@ namespace Microsoft.Dafny {
         Contract.Requires(tickType != null);

         Contract.Requires(setTypeCtor != null);

         Contract.Requires(multiSetTypeCtor != null);

+        Contract.Requires(mapTypeCtor != null);

+        Contract.Requires(arrayLength != null);

         Contract.Requires(seqTypeCtor != null);

         Contract.Requires(fieldNameType != null);

         Contract.Requires(heap != null);

@@ -427,7 +429,7 @@ namespace Microsoft.Dafny {
         {

           var thVar = new Bpl.BoundVariable(ctor.tok, new TypedIdent(ctor.tok, "this", predef.DatatypeType));

           var th = new Bpl.IdentifierExpr(ctor.tok, thVar);

-          var queryPredicate = FunctionCall(ctor.tok, fn.Name, null, th);

+          var queryPredicate = FunctionCall(ctor.tok, fn.Name, Bpl.Type.Bool, th);

           var ctorId = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, th);

           var rhs = Bpl.Expr.Eq(ctorId, new Bpl.IdentifierExpr(ctor.tok, cid));  // this uses the "cid" defined for the previous axiom

           var body = Bpl.Expr.Iff(queryPredicate, rhs);

@@ -552,7 +554,7 @@ namespace Microsoft.Dafny {
       {

         var dVar = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d", predef.DatatypeType));

         var d = new Bpl.IdentifierExpr(dt.tok, dVar);

-        var lhs = FunctionCall(dt.tok, cases_fn.Name, null, d);

+        var lhs = FunctionCall(dt.tok, cases_fn.Name, Bpl.Type.Bool, d);

         Bpl.Expr cases_body = Bpl.Expr.False;

         foreach (DatatypeCtor ctor in dt.Ctors) {

           var disj = FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, d);

@@ -783,10 +785,10 @@ namespace Microsoft.Dafny {
           var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);

           var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));

           var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);

-          var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), null, k, d0, d1);

+          var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1);

           var body = Bpl.Expr.Imp(Bpl.Expr.Le(Bpl.Expr.Literal(0), k), prefixEq);

           var q = new Bpl.ForallExpr(dt.tok, new VariableSeq(kVar), body);

-          var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullCompileName, null, d0, d1);

+          var eqDt = FunctionCall(dt.tok, "$Eq#" + dt.FullCompileName, Bpl.Type.Bool, d0, d1);

           q = new Bpl.ForallExpr(dt.tok, new VariableSeq(d0Var, d1Var), Bpl.Expr.Iff(eqDt, q));

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

         }

@@ -802,8 +804,8 @@ namespace Microsoft.Dafny {
           var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);

           var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));

           var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);

-          var prefixEqK = FunctionCall(dt.tok, CoPrefixName(codecl, 0), null, k, d0, d1);

-          var prefixEqM = FunctionCall(dt.tok, CoPrefixName(codecl, 1), null, m, d0, d1);

+          var prefixEqK = FunctionCall(dt.tok, CoPrefixName(codecl, 0), Bpl.Type.Bool, k, d0, d1);

+          var prefixEqM = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, m, d0, d1);

           var range = BplAnd(Bpl.Expr.Le(Bpl.Expr.Literal(0), k), Bpl.Expr.Le(k, m));

           var body = Bpl.Expr.Imp(BplAnd(range, prefixEqM), prefixEqK);

           var q = new Bpl.ForallExpr(dt.tok, new VariableSeq(kVar, mVar, d0Var, d1Var), body);

@@ -821,7 +823,7 @@ namespace Microsoft.Dafny {
           var d0 = new Bpl.IdentifierExpr(dt.tok, d0Var);

           var d1Var = new Bpl.BoundVariable(dt.tok, new Bpl.TypedIdent(dt.tok, "d1", predef.DatatypeType));

           var d1 = new Bpl.IdentifierExpr(dt.tok, d1Var);

-          var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), null, k, d0, d1);

+          var prefixEq = FunctionCall(dt.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, d0, d1);

           var body = Bpl.Expr.Imp(BplAnd(Bpl.Expr.Eq(d0, d1), Bpl.Expr.Le(Bpl.Expr.Literal(0), k)), prefixEq);

           var q = new Bpl.ForallExpr(dt.tok, new VariableSeq(kVar, d0Var, d1Var), body);

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

@@ -3491,6 +3493,9 @@ namespace Microsoft.Dafny {
       public override string TypeName(ModuleDefinition context) {

         return "_increasingInt";

       }

+      public override bool Equals(Type that) {

+        return that.Normalize() is EverIncreasingType;

+      }

     }

 

     Expression FrameToObjectSet(List<FrameExpression> fexprs) {

@@ -8660,6 +8665,7 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(tok != null);

       Contract.Requires(function != null);

+      Contract.Requires(returnType != null);

       Contract.Requires(args != null);

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

 

@@ -8837,7 +8843,7 @@ namespace Microsoft.Dafny {
           //   checked $PrefixEqual#Dt(k, A, B) || (0 < k ==> A.Cons? ==> B.Cons? && A.head == B.head && $PrefixEqual#2#Dt(k - 1, A.tail, B.tail))  // note the #2 in the recursive call, just like for user-defined predicates that are inlined by TrSplitExpr

           //   free $PrefixEqual#Dt(k, A, B);

           var kPos = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);

-          var prefixEqK = FunctionCall(expr.tok, CoPrefixName(codecl, 1), null, k, A, B);

+          var prefixEqK = FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B);

           var kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));

           // for the inlining of the definition of prefix equality, translate the two main equality operands arguments with a higher offset (to obtain #2 functions)

           var etran2 = etran.LayerOffset(1);

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index e7679a11..ecf2544c 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -124,6 +124,7 @@ namespace Microsoft.Dafny
 

     public static void ErrorWriteLine(string format, params object[] args) {

       Contract.Requires(format != null);

+      Contract.Requires(args != null);

       string s = string.Format(format, args);

       ErrorWriteLine(s);

     }

@@ -192,6 +193,7 @@ namespace Microsoft.Dafny
 

     private static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName)

     {

+      Contract.Requires(dafnyProgram != null);

       // Compile the Dafny program into a string that contains the C# program

       StringWriter sw = new StringWriter();

       Dafny.Compiler compiler = new Dafny.Compiler(sw);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c738f058..879ee8af 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1786,15 +1786,15 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met
 Calculations.dfy(3,4): Error: index out of range

 Execution trace:

     (0,0): anon0

-    (0,0): anon11_Then

+    (0,0): anon17_Then

 Calculations.dfy(8,13): Error: index out of range

 Execution trace:

     (0,0): anon0

-    (0,0): anon13_Then

+    (0,0): anon19_Then

 Calculations.dfy(8,17): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon13_Then

+    (0,0): anon19_Then

 Calculations.dfy(42,11): Error: assertion violation

 Execution trace:

     (0,0): anon0