diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-29 18:11:49 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-29 18:11:49 -0700 |
| commit | 4a522f9458decdf7865be79596788c50e9145faf (patch) | |
| tree | 3ee69980ad3fea1690997b57ba58b633ef74eabe /Test/dafny0/FunctionSpecifications.dfy | |
| parent | 4f26cc2a956771717d21285d9bb527a0602c3e0a (diff) | |
Dafny: fixed bug in checking postconditions of functions that mention the result the function itself
Diffstat (limited to 'Test/dafny0/FunctionSpecifications.dfy')
| -rw-r--r-- | Test/dafny0/FunctionSpecifications.dfy | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy index 13171c47..44709ce8 100644 --- a/Test/dafny0/FunctionSpecifications.dfy +++ b/Test/dafny0/FunctionSpecifications.dfy @@ -52,3 +52,9 @@ function DivergentPost(n: int): int if n < 2 then n else
DivergentPost(n-2) + DivergentPost(n-1)
}
+
+function HoldsAtLeastForZero(x: int): bool
+ ensures x == 0 ==> HoldsAtLeastForZero(x);
+{
+ x < -2 // error: this does not hold for 0
+}
|