From efeb1c5ddde488b4923d87339b8ebbf75d910e16 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 9 Mar 2015 10:12:44 -0700
Subject: 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
---
 Test/dafny2/MonotonicHeapstate.dfy | 6 +++---
 Test/dafny2/StoreAndRetrieve.dfy   | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'Test/dafny2')

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
     }
-- 
cgit v1.2.3