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

diff --git a/Test/dafny0/Protected.dfy b/Test/dafny0/Protected.dfy
new file mode 100644
index 00000000..086a0ae0
--- /dev/null
+++ b/Test/dafny0/Protected.dfy
@@ -0,0 +1,57 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+module Library {

+  function F(): int { 5 }

+  function {:opaque} G(): int { 5 }

+  protected function H(): int { 5 }

+

+  lemma L0() {

+    assert F() == 5;

+    assert H() == 5;

+  }

+  lemma L1() {

+    var t := *;

+    if {

+      case true =>

+        assert G() == 5;  // error: G() is opauqe

+        return;

+      case true =>

+        reveal_G();

+        assert G() == 5;

+      case true =>

+        reveal_G();

+        t := 2;

+      case true =>

+        t := 3;

+    }

+    if t != 3 {

+      assert G() == 5;  // fine, since G() has been revealed on this path, or it's known to be 5

+    } else {

+      assert G() == 5;  // error: G() may not have been revealed

+    }

+  }

+  lemma L2() {

+    assert G() == 5;  // error: G() has not yet been revealed

+    reveal_G();  // revealing afterwards is not good enough

+  }

+  lemma L3() {

+    assert H() == 5;  // yes, definition of H() is known, because we're inside H's defining module

+  }

+}

+

+module Client {

+  import Lib = Library

+

+  lemma L0() {

+    assert Lib.F() == 5;  // yes, because F() is not opaque

+    assert Lib.G() == 5;  // error: not known, since G() is opaque

+  }

+  lemma L1() {

+    Lib.reveal_G();

+    assert Lib.G() == 5;  // yes, the definition has been revealed

+  }

+  lemma L2() {

+    assert Lib.H() == 5;  // error: H() is protected, so its definition is not available

+  }

+}