Compile reals

1 files changed, 29 insertions, 0 deletions

diff --git a/Test/dafny0/RealCompare.dfy b/Test/dafny0/RealCompare.dfy
index 0e4a8c5e..c8320d8a 100644
--- a/Test/dafny0/RealCompare.dfy
+++ b/Test/dafny0/RealCompare.dfy
@@ -123,3 +123,32 @@ method W5(N: real)
     }

   }

 }

+

+method Test_AbsInt0()

+{

+  var a, i := 0.3, 0;

+  while i < 10

+    invariant a == 0.3 + 0.5 * real(i);

+  {

+    a, i := a + 0.5, i + 1;

+  }

+  assert a == 5.3;

+  assert a < 5.9;

+  assert 0.59 <= a;

+  assert a < 0.62;  // error

+}

+

+method Test_AbsInt1()

+{

+  var a, i := 0.3, 0.0;

+  while i < 10.0

+    invariant i <= 10.0 && i == real(int(i));

+    invariant a == 0.3 + 0.5 * i;

+  {

+    a, i := a + 0.5, i + 1.0;

+  }

+  assert a == 5.3;

+  assert a < 5.9;

+  assert 0.59 <= a;

+  assert a < 0.62;  // error

+}