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, 32 insertions, 0 deletions

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

+}