This changeset changes the default visibility of a function/predicate body outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'.

Semantics of 'protected':
* The definition (i.e., body) of a 'protected' function is not visible outside the defining module
* The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions.
* In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected'
* The 'protected' status of a function must be preserved in refinement modules

19 files changed, 207 insertions, 52 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 9501caed..9cad2bb1 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -690,6 +690,8 @@ namespace Microsoft.Dafny
             bool isCoPredicate = f is CoPredicate;

             if (!(member is Function) || (isPredicate && !(member is Predicate)) || (isCoPredicate && !(member is CoPredicate))) {

               reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", f.WhatKind, nwMember.Name);

+            } else if (f.IsProtected != ((Function)member).IsProtected) {

+              reporter.Error(f, "a {0} in a refinement module must be declared 'protected' if and only if the refined {0} is", f.WhatKind);

             } else {

               var prevFunction = (Function)member;

               if (f.Req.Count != 0) {

@@ -726,10 +728,14 @@ namespace Microsoft.Dafny
               Expression replacementBody = null;

               if (prevFunction.Body == null) {

                 replacementBody = f.Body;

-              } else if (isPredicate) {

-                moreBody = f.Body;

               } else if (f.Body != null) {

-                reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");

+                if (isPredicate && f.IsProtected) {

+                  moreBody = f.Body;

+                } else if (isPredicate) {

+                  reporter.Error(nwMember, "a refining predicate is not allowed to extend/change the body unless it is declared 'protected'");

+                } else {

+                  reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");

+                }

               }

               var newF = CloneFunction(f.tok, prevFunction, f.IsGhost, f.Ens, moreBody, replacementBody, prevFunction.Body == null, f.Attributes);

               newF.RefinementBase = member;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index fcc574e3..c16b8710 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -261,7 +261,7 @@ namespace Microsoft.Dafny
       var refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, prog);

       rewriters.Add(refinementTransformer);

       rewriters.Add(new AutoContractsRewriter());

-      var opaqueRewriter = new OpaqueFunctionRewriter();

+      var opaqueRewriter = new OpaqueFunctionRewriter(this);

       rewriters.Add(new AutoReqFunctionRewriter(this, opaqueRewriter));

       rewriters.Add(opaqueRewriter);

       rewriters.Add(new TimeLimitRewriter());

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index f5a9f6b0..12b5adfc 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -386,11 +386,14 @@ namespace Microsoft.Dafny
   /// specifically asks to see it via the reveal_foo() lemma

   /// </summary>

   public class OpaqueFunctionRewriter : IRewriter {

+    readonly ResolutionErrorReporter reporter;

     protected Dictionary<Function, Function> fullVersion; // Given an opaque function, retrieve the full

     protected Dictionary<Function, Function> original;    // Given a full version of an opaque function, find the original opaque version

     protected Dictionary<Lemma, Function> revealOriginal; // Map reveal_* lemmas back to their original functions

 

-    public OpaqueFunctionRewriter() : base() {

+    public OpaqueFunctionRewriter(ResolutionErrorReporter reporter)

+      : base() {

+      this.reporter = reporter;

       fullVersion = new Dictionary<Function, Function>();

       original = new Dictionary<Function, Function>();

       revealOriginal = new Dictionary<Lemma, Function>();

@@ -471,7 +474,11 @@ namespace Microsoft.Dafny
         if (member is Function) {

           var f = (Function)member;

 

-          if (Attributes.Contains(f.Attributes, "opaque") && !RefinementToken.IsInherited(f.tok, c.Module)) {

+          if (!Attributes.Contains(f.Attributes, "opaque")) {

+            // Nothing to do

+          } else if (f.IsProtected) {

+            reporter.Error(f.tok, ":opaque is not allowed to be applied to protected functions (this will be allowed when the language introduces 'opaque'/'reveal' as keywords)");

+          } else if (!RefinementToken.IsInherited(f.tok, c.Module)) {

             // Create a copy, which will be the internal version with a full body

             // which will allow us to verify that the ensures are true

             var cloner = new Cloner();

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index cdc40e2f..a906fb45 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1429,9 +1429,8 @@ namespace Microsoft.Dafny {
           AddClassMember_Function(f);

           if (!IsOpaqueFunction(f) && !f.IsBuiltin && !(f.tok is IncludeToken)) { // Opaque function's well-formedness is checked on the full version

             AddWellformednessCheck(f);

-            if (f.OverriddenFunction != null) //it means that f is overriding its associated parent function

-            {

-                AddFunctionOverrideCheckImpl(f);

+            if (f.OverriddenFunction != null) { //it means that f is overriding its associated parent function

+              AddFunctionOverrideCheckImpl(f);

             }

           }

           var cop = f as CoPredicate;

@@ -1481,12 +1480,29 @@ namespace Microsoft.Dafny {
       }

     }

 

-    private bool IsOpaqueFunction(Function f) {

+    /// <summary>

+    /// Returns true if the body of function "f" is available in module "context".

+    /// This happens when "f" has a body, "f" is not opaque, and either "f" is declared

+    /// in module "context" or "f" is not protected.

+    /// </summary>

+    static bool FunctionBodyIsAvailable(Function f, ModuleDefinition context) {

+      Contract.Requires(f != null);

+      Contract.Requires(context != null);

+      return f.Body != null && !IsOpaqueFunction(f) && (f.EnclosingClass.Module == context || !f.IsProtected);

+    }

+    static bool IsOpaqueFunction(Function f) {

+      Contract.Requires(f != null);

       return Attributes.Contains(f.Attributes, "opaque") &&

             !Attributes.Contains(f.Attributes, "opaque_full");  // The full version has both attributes

     }

 

     private void AddClassMember_Function(Function f) {

+      Contract.Ensures(currentModule == null && codeContext == null);

+      Contract.Ensures(currentModule == null && codeContext == null);

+

+      currentModule = f.EnclosingClass.Module;

+      codeContext = f;

+

       // declare function

       AddFunction(f);

       // add synonym axiom

@@ -1511,6 +1527,8 @@ namespace Microsoft.Dafny {
       if (f is CoPredicate) {

         AddPrefixPredicateAxioms(((CoPredicate)f).PrefixPredicate);

       }

+

+      Reset();

     }

 

     void AddIteratorSpecAndBody(IteratorDecl iter) {

@@ -1609,6 +1627,11 @@ namespace Microsoft.Dafny {
     }

 

     void AddIteratorWellformed(IteratorDecl iter, Procedure proc) {

+      Contract.Requires(iter != null);

+      Contract.Requires(proc != null);

+      Contract.Requires(currentModule == null && codeContext == null);

+      Contract.Ensures(currentModule == null && codeContext == null);

+

       currentModule = iter.Module;

       codeContext = iter;

 

@@ -1920,8 +1943,8 @@ namespace Microsoft.Dafny {
         }

 

         if (!DafnyOptions.O.Dafnycc) {

-            ax = FunctionAxiom(f, visibility, body, f.Formals);

-            sink.AddTopLevelDeclaration(ax);

+          ax = FunctionAxiom(f, visibility, body, f.Formals);

+          sink.AddTopLevelDeclaration(ax);

         }

       }

     }

@@ -2244,7 +2267,7 @@ namespace Microsoft.Dafny {
       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new List<Bpl.Expr> { funcAppl });

       var typeParams = TrTypeParamDecls(f.TypeArgs);

       Bpl.Expr meat;

-      if (visibility == FunctionAxiomVisibility.ForeignModuleOnly /* TODO: add 'public' feature and add: && !IsPublic(f) */) {

+      if (visibility == FunctionAxiomVisibility.ForeignModuleOnly && f.IsProtected) {

         meat = Bpl.Expr.True;

       } else {

         var bodyWithSubst = Substitute(body, null, substMap);

@@ -6018,7 +6041,7 @@ namespace Microsoft.Dafny {
     ///    the first place.

     /// InterModuleCall

     ///    This procedure is suitable for inter-module callers.

-    ///    This means that predicate definitions are not inlined.

+    ///    This means that predicate definitions inlined only for non-protected predicates.

     /// IntraModuleCall

     ///    This procedure is suitable for non-co-call intra-module callers.

     ///    This means that predicates can be inlined in the usual way.

@@ -10646,7 +10669,7 @@ namespace Microsoft.Dafny {
 

           Expr result = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(id), args);

           result = translator.CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type);

-          if (returnLit && !translator.IsOpaqueFunction(e.Function)) {

+          if (returnLit && Translator.FunctionBodyIsAvailable(e.Function, translator.currentModule)) {

             result = translator.Lit(result, ty);

           }

           return result;

@@ -12223,8 +12246,8 @@ namespace Microsoft.Dafny {
 

     /// <summary>

     /// Tries to split the expression into tactical conjuncts (if "position") or disjuncts (if "!position").

-    /// If a (necessarily boolean) function call appears as a top-level conjunct, then inline the function if

-    /// if it declared in the current module and its height is less than "heightLimit" (if "heightLimit" is

+    /// If a (necessarily boolean) function call appears as a top-level conjunct, then inline the function

+    /// if its body is available in the current context and its height is less than "heightLimit" (if "heightLimit" is

     /// passed in as 0, then no functions will be inlined).

     /// </summary>

     bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool position, int heightLimit, bool apply_induction, ExpressionTranslator etran) {

@@ -12400,8 +12423,8 @@ namespace Microsoft.Dafny {
               (codeContext == null || !codeContext.MustReverify)) {

             // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything

             // that needed to be proved about the function was proved already in the previous module, even without the body definition).

-          } else if (IsOpaqueFunction(f)) {

-            // Don't inline opaque functions

+          } else if (!FunctionBodyIsAvailable(f, currentModule)) {

+            // Don't inline opaque functions or foreign protected functions

           } else {

             // inline this body

             var body = GetSubstitutedBody(fexp, f, false);

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 699a730c..505d9b74 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -66,7 +66,7 @@ method Botch1(x: int)
 

 module A_Visibility {

   class C {

-    static predicate P(x: int)

+    protected static predicate P(x: int)

       ensures P(x) ==> -10 <= x;

     {

       0 <= x

diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
index 64e63293..e1c0756c 100644
--- a/Test/dafny0/OpaqueFunctions.dfy
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -4,12 +4,12 @@
 module A {

   class C {

     var x: int;

-    predicate Valid()

+    protected predicate Valid()

       reads this;

     {

       0 <= x

     }

-    function Get(): int

+    protected function Get(): int

       reads this;

     {

       x

@@ -30,7 +30,7 @@ module A {
 }

 module A' refines A {

   class C {

-    predicate Valid...

+    protected predicate Valid...

     {

       x == 8

     }

@@ -55,7 +55,7 @@ module B {
     requires c != null;

     modifies c;

   {

-    assert c.Get() == c.x;  // error because Get() s opaque

+    assert c.Get() == c.x;  // error because Get() is opaque

     if * {

       assert c.Valid();  // error, because Valid() is opaque

     } else if * {

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index b3f36b84..737dacd2 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -4,7 +4,7 @@
 module A {

   class C {

     var x: int;

-    predicate P()

+    protected predicate P()

       reads this;

     {

       x < 100

@@ -26,7 +26,7 @@ module A {
 

 module B refines A {

   class C {

-    predicate P()

+    protected predicate P()

     {

       0 <= x

     }

@@ -39,7 +39,7 @@ module Loose {
   class MyNumber {

     var N: int;

     ghost var Repr: set<object>;

-    predicate Valid()

+    protected predicate Valid()

       reads this, Repr;

     {

       this in Repr && null !in Repr &&

@@ -70,7 +70,7 @@ module Loose {
 

 module Tight refines Loose {

   class MyNumber {

-    predicate Valid()

+    protected predicate Valid()

     {

       N % 2 == 0

     }

@@ -115,7 +115,7 @@ module Tricky_Base {
     {

       x < 10

     }

-    predicate Valid()

+    protected predicate Valid()

       reads this;

     {

       x < 100

@@ -131,7 +131,7 @@ module Tricky_Base {
 

 module Tricky_Full refines Tricky_Base {

   class Tree {

-    predicate Valid()

+    protected predicate Valid()

     {

       Constrained()  // this causes an error to be generated for the inherited Init

     }

@@ -143,7 +143,7 @@ module Tricky_Full refines Tricky_Base {
 module Q0 {

   class C {

     var x: int;

-    predicate P()

+    protected predicate P()

       reads this;

     {

       true

@@ -170,7 +170,7 @@ module Q0 {
 

 module Q1 refines Q0 {

   class C {

-    predicate P()

+    protected predicate P()

     {

       x == 18

     }

diff --git a/Test/dafny0/Protected.dfy b/Test/dafny0/Protected.dfy
new file mode 100644
index 00000000..086a0ae0
--- /dev/null
+++ b/Test/dafny0/Protected.dfy
@@ -0,0 +1,57 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+module Library {

+  function F(): int { 5 }

+  function {:opaque} G(): int { 5 }

+  protected function H(): int { 5 }

+

+  lemma L0() {

+    assert F() == 5;

+    assert H() == 5;

+  }

+  lemma L1() {

+    var t := *;

+    if {

+      case true =>

+        assert G() == 5;  // error: G() is opauqe

+        return;

+      case true =>

+        reveal_G();

+        assert G() == 5;

+      case true =>

+        reveal_G();

+        t := 2;

+      case true =>

+        t := 3;

+    }

+    if t != 3 {

+      assert G() == 5;  // fine, since G() has been revealed on this path, or it's known to be 5

+    } else {

+      assert G() == 5;  // error: G() may not have been revealed

+    }

+  }

+  lemma L2() {

+    assert G() == 5;  // error: G() has not yet been revealed

+    reveal_G();  // revealing afterwards is not good enough

+  }

+  lemma L3() {

+    assert H() == 5;  // yes, definition of H() is known, because we're inside H's defining module

+  }

+}

+

+module Client {

+  import Lib = Library

+

+  lemma L0() {

+    assert Lib.F() == 5;  // yes, because F() is not opaque

+    assert Lib.G() == 5;  // error: not known, since G() is opaque

+  }

+  lemma L1() {

+    Lib.reveal_G();

+    assert Lib.G() == 5;  // yes, the definition has been revealed

+  }

+  lemma L2() {

+    assert Lib.H() == 5;  // error: H() is protected, so its definition is not available

+  }

+}

diff --git a/Test/dafny0/Protected.dfy.expect b/Test/dafny0/Protected.dfy.expect
new file mode 100644
index 00000000..d50f2dd5
--- /dev/null
+++ b/Test/dafny0/Protected.dfy.expect
@@ -0,0 +1,21 @@
+Protected.dfy(17,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+Protected.dfy(31,18): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Then

+    (0,0): anon6

+    (0,0): anon13_Else

+Protected.dfy(35,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Protected.dfy(48,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+Protected.dfy(55,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 14 verified, 5 errors

diff --git a/Test/dafny0/ProtectedResolution.dfy b/Test/dafny0/ProtectedResolution.dfy
new file mode 100644
index 00000000..4e95a452
--- /dev/null
+++ b/Test/dafny0/ProtectedResolution.dfy
@@ -0,0 +1,32 @@
+// RUN: %dafny /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+module J0 {

+  function F0(): int

+  protected function F1(): int

+  predicate R0()

+  protected predicate R1()

+}

+module J1 refines J0 {

+  protected function F0(): int  // error: cannot add 'protected' modifier

+  function F1(): int  // error: cannot drop 'protected' modifier

+  protected predicate R0()  // error: cannot add 'protected' modifier

+  predicate R1()  // error: cannot drop 'protected' modifier

+}

+

+module M0 {

+  function F(): int { 5 }

+  protected function G(): int { 5 }

+  predicate P() { true }

+  protected predicate Q() { true }

+}

+module M1 refines M0 {

+  function F... { 7 }  // error: not allowed to change body

+  protected function G... { 7 }  // error: not allowed to change body

+  predicate P... { true }  // error: not allowed to extend body

+  protected predicate Q... { true }  // fine

+}

+

+module Y0 {

+  protected function {:opaque} F(): int { 5 }  // error: protected and opaque are incompatible

+}

diff --git a/Test/dafny0/ProtectedResolution.dfy.expect b/Test/dafny0/ProtectedResolution.dfy.expect
new file mode 100644
index 00000000..880badcb
--- /dev/null
+++ b/Test/dafny0/ProtectedResolution.dfy.expect
@@ -0,0 +1,9 @@
+ProtectedResolution.dfy(11,21): Error: a function in a refinement module must be declared 'protected' if and only if the refined function is

+ProtectedResolution.dfy(12,11): Error: a function in a refinement module must be declared 'protected' if and only if the refined function is

+ProtectedResolution.dfy(13,22): Error: a predicate in a refinement module must be declared 'protected' if and only if the refined predicate is

+ProtectedResolution.dfy(14,12): Error: a predicate in a refinement module must be declared 'protected' if and only if the refined predicate is

+ProtectedResolution.dfy(24,11): Error: a refining function is not allowed to extend/change the body

+ProtectedResolution.dfy(25,21): Error: a refining function is not allowed to extend/change the body

+ProtectedResolution.dfy(26,12): Error: a refining predicate is not allowed to extend/change the body unless it is declared 'protected'

+ProtectedResolution.dfy(31,31): Error: :opaque is not allowed to be applied to protected functions (this will be allowed when the language introduces 'opaque'/'reveal' as keywords)

+8 resolution/type errors detected in ProtectedResolution.dfy

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index 760b090d..38a1bcb9 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -110,7 +110,7 @@ module Abstract {
   class MyNumber {
     ghost var N: int;
     ghost var Repr: set<object>;
-    predicate Valid()
+    protected predicate Valid()
       reads this, Repr;
     {
       this in Repr && null !in Repr
@@ -144,7 +144,7 @@ module Concrete refines Abstract {
   class MyNumber {
     var a: int;
     var b: int;
-    predicate Valid()
+    protected predicate Valid()
     {
       N == a - b
     }
@@ -181,7 +181,7 @@ module IncorrectConcrete refines Abstract {
   class MyNumber {
     var a: int;
     var b: int;
-    predicate Valid()
+    protected predicate Valid()
     {
       N == 2*a - b
     }
diff --git a/Test/dafny0/Superposition.dfy b/Test/dafny0/Superposition.dfy
index 64eab95d..1ba8e051 100644
--- a/Test/dafny0/Superposition.dfy
+++ b/Test/dafny0/Superposition.dfy
@@ -17,7 +17,7 @@ module M0 {
       r := 8;

     }

 

-    predicate P(x: int)

+    protected predicate P(x: int)

       ensures true;  // this postcondition will not be re-checked in refinements, because it does not mention P itself (or anything else that may change in the refinement)

       ensures x < 60 ==> P(x);

     {

@@ -47,7 +47,7 @@ module M1 refines M0 {
       else {}

     }

 

-    predicate P...  // error: inherited postcondition 'x < 60 ==> P(x)' is violated by this strengthening of P()

+    protected predicate P...  // error: inherited postcondition 'x < 60 ==> P(x)' is violated by this strengthening of P()

     {

       false  // with this strengthening of P(), the postcondition fails (still, note that only one of the postconditions is re-checked)

     }

diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect
index 2e988bfb..4b8e354f 100644
--- a/Test/dafny0/Superposition.dfy.expect
+++ b/Test/dafny0/Superposition.dfy.expect
@@ -32,7 +32,7 @@ Verifying Impl$$_1_M1.C.M ...
 

 Verifying CheckWellformed$$_1_M1.C.P ...

   [2 proof obligations]  error

-Superposition.dfy(50,15): Error BP5003: A postcondition might not hold on this return path.

+Superposition.dfy(50,25): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index d61f92ac..8ad86f3b 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -51,11 +51,11 @@ Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
   >>> DoNothingToAssert

 Processing command (at Snapshots2.v0.dfy(11,11)) assert true;

   >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap));

+Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);

   >>> DoNothingToAssert

 Processing command (at Snapshots2.v0.dfy(14,11)) assert true;

   >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.R($Heap));

+Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));

   >>> DoNothingToAssert

 Processing command (at Snapshots2.v0.dfy(18,3)) assert true;

   >>> DoNothingToAssert

@@ -74,11 +74,11 @@ Execution trace:
     (0,0): anon0

 Processing command (at Snapshots2.v1.dfy(11,11)) assert true;

   >>> MarkAsFullyVerified

-Processing command (at Snapshots2.v1.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap));

+Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);

   >>> DoNothingToAssert

 Processing command (at Snapshots2.v1.dfy(14,11)) assert true;

   >>> MarkAsFullyVerified

-Processing command (at Snapshots2.v1.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.R($Heap));

+Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));

   >>> DoNothingToAssert

 

 Dafny program verifier finished with 5 verified, 1 error

diff --git a/Test/dafny2/MonotonicHeapstate.dfy b/Test/dafny2/MonotonicHeapstate.dfy
index d6817ce9..b0032b44 100644
--- a/Test/dafny2/MonotonicHeapstate.dfy
+++ b/Test/dafny2/MonotonicHeapstate.dfy
@@ -12,7 +12,7 @@ module M0 {
 

     ghost var Repr: set<object>;

 

-    predicate Valid()

+    protected predicate Valid()

       reads this, Repr;

     {

       this in Repr && null !in Repr &&

@@ -58,7 +58,7 @@ module M1 refines M0 {
   class Expr {

     ghost var resolved: bool;

 

-    predicate Valid()

+    protected predicate Valid()

     {

       resolved ==>

         (kind == Binary ==> left.resolved && right.resolved)

@@ -104,7 +104,7 @@ module M2 refines M1 {
   class Expr {

     var decl: VarDecl;  // if kind==Ident, filled in during resolution

 

-    predicate Valid()

+    protected predicate Valid()

     {

       resolved ==>

         (kind == Ident ==> decl != null)

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index e39913a8..5314b6fa 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -5,7 +5,7 @@ abstract module A {
   import L = Library

   class {:autocontracts} StoreAndRetrieve<Thing(==)> {

     ghost var Contents: set<Thing>;

-    predicate Valid()

+    protected predicate Valid()

     {

       true

     }

@@ -31,7 +31,7 @@ abstract module A {
 module B refines A {

   class StoreAndRetrieve<Thing(==)> {

     var arr: seq<Thing>;

-    predicate Valid()

+    protected predicate Valid()

     {

       Contents == set x | x in arr

     }

diff --git a/Test/dafny3/CachedContainer.dfy b/Test/dafny3/CachedContainer.dfy
index a3824fbf..03aef62d 100644
--- a/Test/dafny3/CachedContainer.dfy
+++ b/Test/dafny3/CachedContainer.dfy
@@ -5,7 +5,7 @@
 abstract module M0 {

   class {:autocontracts} Container<T(==)> {

     ghost var Contents: set<T>;

-    predicate Valid()

+    protected predicate Valid()

     constructor ()

       ensures Contents == {};

     method Add(t: T)

@@ -41,7 +41,7 @@ abstract module M1 refines M0 {
 module M2 refines M1 {

   class Container<T(==)> {

     var elems: seq<T>;

-    predicate Valid()

+    protected predicate Valid()

     {

       Contents == (set x | x in elems) &&

       forall i,j :: 0 <= i < j < |elems| ==> elems[i] != elems[j]

@@ -89,7 +89,7 @@ module M3 refines M2 {
   class Container<T(==)> {

     var cachedValue: T;

     var cachedIndex: int;

-    predicate Valid() {

+    protected predicate Valid() {

       0 <= cachedIndex ==> cachedIndex < |elems| && elems[cachedIndex] == cachedValue

     }

     constructor... {

diff --git a/Test/dafny4/ClassRefinement.dfy b/Test/dafny4/ClassRefinement.dfy
index cff6d98f..b5ecfbfa 100644
--- a/Test/dafny4/ClassRefinement.dfy
+++ b/Test/dafny4/ClassRefinement.dfy
@@ -12,7 +12,7 @@ abstract module M0 {
   class Counter {

     ghost var N: int;

     ghost var Repr: set<object>;

-    predicate Valid()

+    protected predicate Valid()

       reads this, Repr;

     {

       this in Repr

@@ -51,7 +51,7 @@ module M1 refines M0 {
   class Counter {

     var c: Cell;

     var d: Cell;

-    predicate Valid...

+    protected predicate Valid...

     {

       c != null && c in Repr &&

       d != null && d in Repr &&