Added Equals method on Type

Fixed some precondition violations
Various improvements in Contracts

1 files changed, 2 insertions, 0 deletions

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