diff options
| author |  Rustan Leino <unknown> | 2014-02-13 21:10:16 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-13 21:10:16 -0800 |
| commit | 79610237eba7902e8be127fa54f2572a2c01f6b7 (patch) | |
| tree | 4c273b46c76e2128cc9e058aebdb96d0c6405bc2 /Test/dafny0/RealTypes.dfy | |
| parent | 6897d8be8a9c5ebef140398f682021acfea393bb (diff) | |
Allow unary minus on reals
Diffstat (limited to 'Test/dafny0/RealTypes.dfy')
| -rw-r--r-- | Test/dafny0/RealTypes.dfy | 10 |
1 files changed, 8 insertions, 2 deletions
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;
}
|