diff options
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
+}
|