diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/RealTypes.dfy | 10 |
2 files changed, 9 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 5297d132..a41cd0cd 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -161,7 +161,7 @@ RealTypes.dfy(19,12): Error: assertion violation Execution trace:
(0,0): anon0
-Dafny program verifier finished with 4 verified, 4 errors
+Dafny program verifier finished with 6 verified, 4 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/RealTypes.dfy b/Test/dafny0/RealTypes.dfy index c2d88074..9354bc9d 100644 --- a/Test/dafny0/RealTypes.dfy +++ b/Test/dafny0/RealTypes.dfy @@ -22,6 +22,12 @@ method R3() { // Check that real value in decreases clause doesn't scare Dafny
function R4(x:int, r:real) : int
{
- if x < 0 then 5
- else R4(x - 1, r)
+ if x < 0 then 5
+ else R4(x - 1, r)
+}
+
+method RoundingDirection()
+{
+ assert int(51.500277) == 51;
+ assert int(-0.194771) == -1;
}
|