From d15bd26e93c0398c422526ff9a51fcd445c1e232 Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Fri, 22 Jun 2012 17:52:24 -0700
Subject: Dafny: added contracts to IRewriter methods

---
 Dafny/RefinementTransformer.cs |  5 +----
 Dafny/Resolver.cs              |  2 +-
 Dafny/Rewriter.cs              | 15 +++++++++++++--
 3 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index e3b778d8..bbc12d6a 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -50,7 +50,7 @@ namespace Microsoft.Dafny {
     }
   }
 
-  public class RefinementTransformer : Rewriter
+  public class RefinementTransformer : IRewriter
   {
     ResolutionErrorReporter reporter;
     public RefinementTransformer(ResolutionErrorReporter reporter) {
@@ -62,7 +62,6 @@ namespace Microsoft.Dafny {
     private Queue<Action> postTasks = new Queue<Action>();  // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction
 
     public void PreResolve(ModuleDecl m) {
-      Contract.Requires(m != null);
       if (m.RefinementBase == null) {
         // This Rewriter doesn't do anything
         return;
@@ -153,8 +152,6 @@ namespace Microsoft.Dafny {
     }
 
     public void PostResolve(ModuleDecl m) {
-      Contract.Requires(m != null);
-
       if (m == moduleUnderConstruction) {
         while (this.postTasks.Count != 0) {
           var a = postTasks.Dequeue();
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index ca7a0c69..29aa3bd7 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -170,7 +170,7 @@ namespace Microsoft.Dafny {
       }
 
       // register top-level declarations
-      var rewriters = new List<Rewriter>();
+      var rewriters = new List<IRewriter>();
       // The following line could be generalized to allow rewriter plug-ins; to support such, just add command-line
       // switches and .Add to "rewriters" here.
       rewriters.Add(new AutoContractsRewriter());
diff --git a/Dafny/Rewriter.cs b/Dafny/Rewriter.cs
index 26ec496e..e04c5e9b 100644
--- a/Dafny/Rewriter.cs
+++ b/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) {
-- 
cgit v1.2.3