1 files changed, 13 insertions, 2 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 26ec496e..e04c5e9b 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -4,11 +4,22 @@ using System.Diagnostics.Contracts;
 
 namespace Microsoft.Dafny
 {
-  public interface Rewriter
+  [ContractClass(typeof(IRewriterContracts))]
+  public interface IRewriter
   {
     void PreResolve(ModuleDecl m);
     void PostResolve(ModuleDecl m);
   }
+  [ContractClassFor(typeof(IRewriter))]
+  abstract class IRewriterContracts : IRewriter
+  {
+    public void PreResolve(ModuleDecl m) {
+      Contract.Requires(m != null);
+    }
+    public void PostResolve(ModuleDecl m) {
+      Contract.Requires(m != null);
+    }
+  }
 
   /// <summary>
   /// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate
@@ -48,7 +59,7 @@ namespace Microsoft.Dafny
   ///    if (A != null) { Repr := Repr + {A}; }
   ///    if (F != null) { Repr := Repr + {F} + F.Repr; }
   /// </summary>
-  public class AutoContractsRewriter : Rewriter
+  public class AutoContractsRewriter : IRewriter
   {
     public void PreResolve(ModuleDecl m) {
       foreach (var d in m.TopLevelDecls) {