diff options
| author |  leino <unknown> | 2015-03-09 10:12:44 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-03-09 10:12:44 -0700 |
| commit | efeb1c5ddde488b4923d87339b8ebbf75d910e16 (patch) | |
| tree | dc44c9b431f1f24889047b736d8720c2a89d794e /Test/dafny0/ProtectedResolution.dfy.expect | |
| parent | 1157b689cbc7c65cde1f20192e8b3b49046d6fc4 (diff) | |
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
Diffstat (limited to 'Test/dafny0/ProtectedResolution.dfy.expect')
| -rw-r--r-- | Test/dafny0/ProtectedResolution.dfy.expect | 9 |
1 files changed, 9 insertions, 0 deletions
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
|