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

11 files changed, 142 insertions, 23 deletions

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 699a730c..505d9b74 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -66,7 +66,7 @@ method Botch1(x: int)
 

 module A_Visibility {

   class C {

-    static predicate P(x: int)

+    protected static predicate P(x: int)

       ensures P(x) ==> -10 <= x;

     {

       0 <= x

diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
index 64e63293..e1c0756c 100644
--- a/Test/dafny0/OpaqueFunctions.dfy
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -4,12 +4,12 @@
 module A {

   class C {

     var x: int;

-    predicate Valid()

+    protected predicate Valid()

       reads this;

     {

       0 <= x

     }

-    function Get(): int

+    protected function Get(): int

       reads this;

     {

       x

@@ -30,7 +30,7 @@ module A {
 }

 module A' refines A {

   class C {

-    predicate Valid...

+    protected predicate Valid...

     {

       x == 8

     }

@@ -55,7 +55,7 @@ module B {
     requires c != null;

     modifies c;

   {

-    assert c.Get() == c.x;  // error because Get() s opaque

+    assert c.Get() == c.x;  // error because Get() is opaque

     if * {

       assert c.Valid();  // error, because Valid() is opaque

     } else if * {

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index b3f36b84..737dacd2 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -4,7 +4,7 @@
 module A {

   class C {

     var x: int;

-    predicate P()

+    protected predicate P()

       reads this;

     {

       x < 100

@@ -26,7 +26,7 @@ module A {
 

 module B refines A {

   class C {

-    predicate P()

+    protected predicate P()

     {

       0 <= x

     }

@@ -39,7 +39,7 @@ module Loose {
   class MyNumber {

     var N: int;

     ghost var Repr: set<object>;

-    predicate Valid()

+    protected predicate Valid()

       reads this, Repr;

     {

       this in Repr && null !in Repr &&

@@ -70,7 +70,7 @@ module Loose {
 

 module Tight refines Loose {

   class MyNumber {

-    predicate Valid()

+    protected predicate Valid()

     {

       N % 2 == 0

     }

@@ -115,7 +115,7 @@ module Tricky_Base {
     {

       x < 10

     }

-    predicate Valid()

+    protected predicate Valid()

       reads this;

     {

       x < 100

@@ -131,7 +131,7 @@ module Tricky_Base {
 

 module Tricky_Full refines Tricky_Base {

   class Tree {

-    predicate Valid()

+    protected predicate Valid()

     {

       Constrained()  // this causes an error to be generated for the inherited Init

     }

@@ -143,7 +143,7 @@ module Tricky_Full refines Tricky_Base {
 module Q0 {

   class C {

     var x: int;

-    predicate P()

+    protected predicate P()

       reads this;

     {

       true

@@ -170,7 +170,7 @@ module Q0 {
 

 module Q1 refines Q0 {

   class C {

-    predicate P()

+    protected predicate P()

     {

       x == 18

     }

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

+  }

+}

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

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

+}

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

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index 760b090d..38a1bcb9 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -110,7 +110,7 @@ module Abstract {
   class MyNumber {
     ghost var N: int;
     ghost var Repr: set<object>;
-    predicate Valid()
+    protected predicate Valid()
       reads this, Repr;
     {
       this in Repr && null !in Repr
@@ -144,7 +144,7 @@ module Concrete refines Abstract {
   class MyNumber {
     var a: int;
     var b: int;
-    predicate Valid()
+    protected predicate Valid()
     {
       N == a - b
     }
@@ -181,7 +181,7 @@ module IncorrectConcrete refines Abstract {
   class MyNumber {
     var a: int;
     var b: int;
-    predicate Valid()
+    protected predicate Valid()
     {
       N == 2*a - b
     }
diff --git a/Test/dafny0/Superposition.dfy b/Test/dafny0/Superposition.dfy
index 64eab95d..1ba8e051 100644
--- a/Test/dafny0/Superposition.dfy
+++ b/Test/dafny0/Superposition.dfy
@@ -17,7 +17,7 @@ module M0 {
       r := 8;

     }

 

-    predicate P(x: int)

+    protected predicate P(x: int)

       ensures true;  // this postcondition will not be re-checked in refinements, because it does not mention P itself (or anything else that may change in the refinement)

       ensures x < 60 ==> P(x);

     {

@@ -47,7 +47,7 @@ module M1 refines M0 {
       else {}

     }

 

-    predicate P...  // error: inherited postcondition 'x < 60 ==> P(x)' is violated by this strengthening of P()

+    protected predicate P...  // error: inherited postcondition 'x < 60 ==> P(x)' is violated by this strengthening of P()

     {

       false  // with this strengthening of P(), the postcondition fails (still, note that only one of the postconditions is re-checked)

     }

diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect
index 2e988bfb..4b8e354f 100644
--- a/Test/dafny0/Superposition.dfy.expect
+++ b/Test/dafny0/Superposition.dfy.expect
@@ -32,7 +32,7 @@ Verifying Impl$$_1_M1.C.M ...
 

 Verifying CheckWellformed$$_1_M1.C.P ...

   [2 proof obligations]  error

-Superposition.dfy(50,15): Error BP5003: A postcondition might not hold on this return path.

+Superposition.dfy(50,25): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index d61f92ac..8ad86f3b 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -51,11 +51,11 @@ Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
   >>> DoNothingToAssert

 Processing command (at Snapshots2.v0.dfy(11,11)) assert true;

   >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap));

+Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);

   >>> DoNothingToAssert

 Processing command (at Snapshots2.v0.dfy(14,11)) assert true;

   >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.R($Heap));

+Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));

   >>> DoNothingToAssert

 Processing command (at Snapshots2.v0.dfy(18,3)) assert true;

   >>> DoNothingToAssert

@@ -74,11 +74,11 @@ Execution trace:
     (0,0): anon0

 Processing command (at Snapshots2.v1.dfy(11,11)) assert true;

   >>> MarkAsFullyVerified

-Processing command (at Snapshots2.v1.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap));

+Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);

   >>> DoNothingToAssert

 Processing command (at Snapshots2.v1.dfy(14,11)) assert true;

   >>> MarkAsFullyVerified

-Processing command (at Snapshots2.v1.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.R($Heap));

+Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));

   >>> DoNothingToAssert

 

 Dafny program verifier finished with 5 verified, 1 error