Dafny: added contracts to IRewriter methods

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