Dafny: allow self-calls in function postconditions--these simply refer to the result value of the current call

4 files changed, 83 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 450b69bc..71fe813b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -280,6 +280,29 @@ Execution trace:
 

 Dafny program verifier finished with 23 verified, 32 errors

 

+-------------------- FunctionSpecifications.dfy --------------------

+FunctionSpecifications.dfy(31,13): Error: possible violation of function postcondition

+Execution trace:

+    (0,0): anon10_Else

+    (0,0): anon11_Else

+    (0,0): anon12_Then

+    (0,0): anon13_Else

+    (0,0): anon7

+    (0,0): anon9

+FunctionSpecifications.dfy(40,18): Error: possible violation of function postcondition

+Execution trace:

+    (0,0): anon12_Else

+    (0,0): anon15_Else

+    (0,0): anon16_Then

+    (0,0): anon11

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon9_Then

+    (0,0): anon3

+

+Dafny program verifier finished with 3 verified, 3 errors

+

 -------------------- Array.dfy --------------------

 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 1cb74b1d..d4a39179 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -235,7 +235,7 @@ function Postie1(c: Mountain): Mountain
 

 function Postie2(c: Mountain): Mountain

   requires c != null && c.x == 5;

-  ensures Postie2(c).x == 5;  // well-formedness error (null dereference)

+  ensures Postie2(c).x == 5;  // error: well-formedness error (null dereference)

 {

   c

 }

diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy
new file mode 100644
index 00000000..21ce5468
--- /dev/null
+++ b/Test/dafny0/FunctionSpecifications.dfy
@@ -0,0 +1,57 @@
+function Fib(n: int): int

+  requires 0 <= n;

+  ensures 0 <= Fib(n);

+{

+  if n < 2 then n else

+  Fib(n-2) + Fib(n-1)

+}

+

+datatype List {

+  Nil;

+  Cons(int, List);

+}

+

+function Sum(a: List): int

+  ensures 0 <= Sum(a);

+{

+  match a

+  case Nil => 0

+  case Cons(x, tail) => if x < 0 then 0 else Fib(x)

+}

+

+function FibWithoutPost(n: int): int

+  requires 0 <= n;

+{

+  if n < 2 then n else

+  FibWithoutPost(n-2) + FibWithoutPost(n-1)

+}

+

+function SumBad(a: List): int

+  ensures 0 <= Sum(a);  // this is still okay, because this is calling the good Sum

+  ensures 0 <= SumBad(a);  // error: cannot prove postcondition

+{

+  match a

+  case Nil => 0

+  case Cons(x, tail) => if x < 0 then 0 else FibWithoutPost(x)

+}

+

+function FibWithExtraPost(n: int): int

+  ensures 2 <= n ==> 0 <= FibWithExtraPost(n-1); // This is fine, because the definition of the function is discovered via canCall

+  ensures 1 <= n ==> 0 <= FibWithExtraPost(n-1); // Error: In the current implementation of Dafny, one needs to actually call the

+                                                 // function in order to benefit from canCall.  This may be improved in the future.

+  ensures 0 <= FibWithExtraPost(n);

+{

+  if n < 0 then 0 else

+  if n < 2 then n else

+  FibWithExtraPost(n-2) + FibWithExtraPost(n-1)

+}

+

+function DivergentPost(n: int): int

+  requires 0 <= n;

+  ensures 1 <= n ==> DivergentPost(n-1) == DivergentPost(n-1);

+  ensures DivergentPost(2*n - n) == DivergentPost(2*(n+5) - 10 - n);  // these are legal ways to denote the result value of the function

+  ensures DivergentPost(n+1) == DivergentPost(n+1);  // error: call may not terminate

+{

+  if n < 2 then n else

+  DivergentPost(n-2) + DivergentPost(n-1)

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 16596fa5..c92ae0a2 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -11,7 +11,8 @@ for %%f in (Simple.dfy) do (
   %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f

 )

 

-for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy MultiDimArray.dfy

+for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy

+            Array.dfy MultiDimArray.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Refinement.dfy RefinementErrors.dfy) do (