Make functions and predicates be opaque outside the defining module -- only their specifications (e.g., ensures clauses) are exported.

6 files changed, 216 insertions, 14 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c1e04f2a..da6d1caa 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -624,15 +624,15 @@ Modules0.dfy(97,14): Error: Undeclared top-level type or type parameter: MyClass
 28 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

-Modules1.dfy(75,16): Error: assertion violation

+Modules1.dfy(76,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-Modules1.dfy(88,16): Error: assertion violation

+Modules1.dfy(89,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-Modules1.dfy(90,14): Error: assertion violation

+Modules1.dfy(91,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

@@ -1557,6 +1557,80 @@ Execution trace:
 

 Dafny program verifier finished with 9 verified, 1 error

 

+-------------------- OpaqueFunctions.dfy --------------------

+OpaqueFunctions.dfy(24,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(49,7): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy(21,16): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(55,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(57,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+OpaqueFunctions.dfy(60,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+OpaqueFunctions.dfy(63,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+OpaqueFunctions.dfy(74,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+OpaqueFunctions.dfy(76,9): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy[A'](21,16): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+OpaqueFunctions.dfy(83,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(85,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+OpaqueFunctions.dfy(88,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+OpaqueFunctions.dfy(91,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+OpaqueFunctions.dfy(102,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+OpaqueFunctions.dfy(104,9): Error BP5002: A precondition for this call might not hold.

+OpaqueFunctions.dfy[A'](21,16): Related location: This is the precondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+OpaqueFunctions.dfy(111,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+OpaqueFunctions.dfy(113,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+OpaqueFunctions.dfy(116,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+OpaqueFunctions.dfy(119,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Else

+

+Dafny program verifier finished with 32 verified, 18 errors

+

 -------------------- Maps.dfy --------------------

 Maps.dfy(76,8): Error: element may not be in domain

 Execution trace:

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 1f47f3b1..e9c432f3 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -64,6 +64,7 @@ method Botch1(x: int)
 module A_Visibility {

   class C {

     static predicate P(x: int)

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

     {

       0 <= x

     }

@@ -84,8 +85,8 @@ module B_Visibility {
   method Main() {

     var y;

     if (A.C.P(y)) {

-      assert 0 <= y;  // this much is known of C.P

-      assert 2 <= y;  // error

+      assert -10 <= y;  // this much is known of C.P

+      assert 0 <= y;  // error

     } else {

       assert A.C.P(8);  // error: C.P cannot be established outside the declaring module

     }

diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
new file mode 100644
index 00000000..c15515d2
--- /dev/null
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -0,0 +1,123 @@
+module A {

+  class C {

+    var x: int;

+    predicate Valid()

+      reads this;

+    {

+      0 <= x

+    }

+    function Get(): int

+      reads this;

+    {

+      x

+    }

+    constructor ()

+      modifies this;

+      ensures Valid();

+    {

+      x := 8;

+    }

+    method M()

+      requires Valid();

+    {

+      assert Get() == x;

+      assert x == 8;  // error

+    }

+  }

+}

+module A' refines A {

+  class C {

+    predicate Valid...

+    {

+      x == 8

+    }

+    method N()

+      requires Valid();

+    {

+      assert Get() == x;

+      assert x == 8;

+    }

+  }

+}

+

+module B {

+  import X as A

+  method Main() {

+    var c := new X.C();

+    c.M();  // fine

+    c.x := c.x + 1;

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

+  }

+  method L(c: X.C)

+    requires c != null;

+    modifies c;

+  {

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

+    if * {

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

+    } else if * {

+      c.x := 7;

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

+    } else {

+      c.x := 8;

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

+    }

+  }

+}

+module B_direct {

+  import X as A'

+  method Main() {

+    var c := new X.C();

+    c.M();  // fine

+    c.x := c.x + 1;

+    if * {

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

+    } else {

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

+    }

+  }

+  method L(c: X.C)

+    requires c != null;

+    modifies c;

+  {

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

+    if * {

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

+    } else if * {

+      c.x := 7;

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

+    } else {

+      c.x := 8;

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

+    }

+  }

+}

+module B' refines B {

+  import X = A'  // this by itself produces no more error

+  method Main'() {

+    var c := new X.C();

+    c.M();  // fine

+    c.x := c.x + 1;

+    if * {

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

+    } else {

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

+    }

+  }

+  method L'(c: X.C)

+    requires c != null;

+    modifies c;

+  {

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

+    if * {

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

+    } else if * {

+      c.x := 7;

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

+    } else {

+      c.x := 8;

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

+    }

+  }

+}

+

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 1610d8b8..d48b1a6a 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -130,7 +130,7 @@ module Tricky_Full refines Tricky_Base {
   class Tree {

     predicate Valid()

     {

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

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

     }

   }

 }

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index e5c06a5e..3c7563a0 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -101,7 +101,7 @@ module Abstract {
   class MyNumber {
     ghost var N: int;
     ghost var Repr: set<object>;
-    predicate Valid
+    predicate Valid()
       reads this, Repr;
     {
       this in Repr && null !in Repr
@@ -109,20 +109,20 @@ module Abstract {
     constructor Init()
       modifies this;
       ensures N == 0;
-      ensures Valid && fresh(Repr - {this});
+      ensures Valid() && fresh(Repr - {this});
     {
       N, Repr := 0, {this};
     }
     method Inc()
-      requires Valid;
+      requires Valid();
       modifies Repr;
       ensures N == old(N) + 1;
-      ensures Valid && fresh(Repr - old(Repr));
+      ensures Valid() && fresh(Repr - old(Repr));
     {
       N := N + 1;
     }
     method Get() returns (n: int)
-      requires Valid;
+      requires Valid();
       ensures n == N;
     {
       var k;  assume k == N;
@@ -135,7 +135,7 @@ module Concrete refines Abstract {
   class MyNumber {
     var a: int;
     var b: int;
-    predicate Valid
+    predicate Valid()
     {
       N == a - b
     }
@@ -172,7 +172,7 @@ module IncorrectConcrete refines Abstract {
   class MyNumber {
     var a: int;
     var b: int;
-    predicate Valid
+    predicate Valid()
     {
       N == 2*a - b
     }
@@ -191,3 +191,6 @@ module IncorrectConcrete refines Abstract {
     }
   }
 }
+
+// ------------- visibility checks -------------------------------
+
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 18f34345..b911625b 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -23,7 +23,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy

-            Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

+            Predicates.dfy Skeletons.dfy OpaqueFunctions.dfy

+            Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

             Calculations.dfy IteratorResolution.dfy Iterators.dfy

             RankPos.dfy RankNeg.dfy