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

1 files changed, 3 insertions, 3 deletions

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