Added support for opaque function definitions, indicated via the {:opaque} attribute.

Dafny cannot see the body of opaque function foo() unless you call
the (automatically generated) lemma reveal_foo().  This can be helpful in preventing Dafny
from spending unnecessary time thinking about the body of a function.

2 files changed, 150 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4130ebe7..5ac570f3 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -343,8 +343,58 @@ FunctionSpecifications.dfy(57,22): Related location: This is the postcondition t
 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

+FunctionSpecifications.dfy(105,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+FunctionSpecifications.dfy(108,23): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+FunctionSpecifications.dfy(123,27): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+FunctionSpecifications.dfy(127,27): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+FunctionSpecifications.dfy(150,15): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+FunctionSpecifications.dfy(162,3): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+FunctionSpecifications.dfy(169,15): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+FunctionSpecifications.dfy(178,3): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+FunctionSpecifications.dfy(132,20): Error BP5003: A postcondition might not hold on this return path.

+FunctionSpecifications.dfy(134,29): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Else

+FunctionSpecifications.dfy(143,3): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+FunctionSpecifications.dfy(157,3): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+FunctionSpecifications.dfy(185,3): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+FunctionSpecifications.dfy(182,20): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 8 verified, 4 errors

+Dafny program verifier finished with 19 verified, 17 errors

 

 -------------------- ResolutionErrors.dfy --------------------

 ResolutionErrors.dfy(497,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy
index cd38d3dd..b3c6c7bc 100644
--- a/Test/dafny0/FunctionSpecifications.dfy
+++ b/Test/dafny0/FunctionSpecifications.dfy
@@ -87,3 +87,102 @@ function IncC(i: nat): int
 {

   var n :| n>i; n

 }

+

+

+/////////////////////////////////////////////////////////////

+//  Test :opaque functions

+/////////////////////////////////////////////////////////////

+

+// Test basic function hiding

+function {:opaque} secret(x:int, y:int) : int 

+  requires 0 <= x < 5;

+  requires 0 <= y < 5;

+  ensures secret(x, y) < 10;

+{ x + y }

+

+method test_secret()

+{

+  assert secret(2, 3) >= 5;   // Should fail because secret's body is hidden

+  reveal_secret();

+  assert secret(2, 3) == 5;   // Should pass now that the body is "visible" 

+  assert secret(4, 1) == 7;   // Make sure it catches incorrect applications as well

+}

+

+// Check that opaque doesn't break recursion unrolling

+// Also checks that opaque functions that do terminate are verified as such

+function {:opaque} recursive_f(x:int) : int

+  requires x >= 0;

+{

+  if x == 0 then 0

+  else 1 + recursive_f(x - 1)

+}

+

+method test_recursive_f()

+{

+  if * {

+    assert recursive_f(4) == 4;   // Should fail because body is hidden

+  } else {

+    reveal_recursive_f();

+    assert recursive_f(4) == 4;   // Should pass now body is visible and can be unrolled

+    assert recursive_f(3) == 5;   // Make sure it catches incorrect applications as well

+  }

+}

+

+// Check that opaque doesn't interfere with ensures checking

+function {:opaque} bad_ensures(x:int, y:int):int 

+  requires x >= 0 && y >= 0;

+  ensures bad_ensures(x, y) > 0;

+{

+  x + y

+}

+

+// Check that opaque doesn't interfere with termination checking

+function {:opaque} f(i:int):int

+  decreases i;

+{

+  f(i) + 1

+}

+

+method m()

+  ensures false;

+{

+  reveal_f();

+  assert f(0) == f(0) + 1;

+}

+

+// Try a sneakier (nested) version of the test above

+function {:opaque} g(i:int):int

+  decreases i;

+{

+  h(i) + 1

+}

+

+function h(i:int):int

+{

+  g(i)

+}

+

+method n()

+  ensures false;

+{

+  reveal_g();

+  assert g(0) == g(0) + 1;

+}

+

+// Check that using the reveal_ lemma to prove the well-definedness of a function 

+// in a lower SCC does not cause a soundness problem

+

+function A(): int

+  ensures A() == 5;

+{

+  reveal_B();  // error: should not be allowed to invoke reveal_B() here

+  6  // this result value is not what the postcondition specification says

+}

+

+function {:opaque} B(): int

+  ensures B() == 5;

+{

+  A()

+}

+

+