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

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