diff options
| author |  Rustan Leino <unknown> | 2014-04-08 08:32:27 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-08 08:32:27 -0700 |
| commit | 6f107980cd0e5df0e4e5f1ed69b858b811909438 (patch) | |
| tree | c863e87d458a85d569cd5ff9255f182d25cd713c /Test/dafny0/RealCompare.dfy | |
| parent | 75430d038249b6a31eaa63e5c3259b3140382a5d (diff) | |
Allow reals in decreases clauses
Diffstat (limited to 'Test/dafny0/RealCompare.dfy')
| -rw-r--r-- | Test/dafny0/RealCompare.dfy | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/Test/dafny0/RealCompare.dfy b/Test/dafny0/RealCompare.dfy new file mode 100644 index 00000000..0e4a8c5e --- /dev/null +++ b/Test/dafny0/RealCompare.dfy @@ -0,0 +1,125 @@ +method M(x: real)
+ decreases x;
+{
+ if 0.0 <= x {
+ M(x - 15.0);
+ }
+}
+
+method N(x: real, y: real)
+ decreases x, y;
+{
+ if 0.0 <= y {
+ N(x, y - 1.0);
+ } else if 0.0 <= x {
+ N(x - 1.0, 300.0);
+ }
+}
+
+method N_implicitDecreases(x: real, y: real)
+{
+ if 0.0 <= y {
+ N_implicitDecreases(x, y - 1.0);
+ } else if 0.0 <= x {
+ N_implicitDecreases(x - 1.0, 300.0);
+ }
+}
+
+method P(x: real)
+ decreases x;
+{
+ if 0.0 <= x {
+ P(x - 0.5); // error: don't descease enough
+ }
+}
+
+method Q(x: real)
+ decreases 2.0 * x;
+{
+ if 0.0 <= x {
+ Q(x - 0.5); // fine
+ }
+}
+
+method R(x: real)
+ decreases x;
+{
+ R(x - 1.0); // error: no lower bound
+}
+
+method W0(N: real)
+{
+ var i := 0.0;
+ while i < N
+ decreases N - i;
+ {
+ i := i + 1.0;
+ }
+}
+
+method W1(N: real)
+{
+ var i := 0.0;
+ while i < N
+ {
+ i := i + 1.0;
+ }
+}
+
+method W2(N: real)
+{
+ var i, n := 0.0, N;
+ while i < n
+ decreases n - i;
+ {
+ if * {
+ i := i + 1.0;
+ } else {
+ n := n - 1.0;
+ }
+ }
+}
+
+method W3(N: real)
+{
+ var i, n := 0.0, N;
+ while i < n
+ {
+ if * {
+ i := i + 1.0;
+ } else {
+ n := n - 1.0;
+ }
+ }
+}
+
+method W4(N: real)
+{
+ var i, n := 0.0, N;
+ while i != n
+ decreases if i < n then n - i else i - n; // absolute value
+ {
+ if i < n {
+ i := i + 1.0;
+ if n < i { break; }
+ } else {
+ n := n + 1.0;
+ if i < n { break; }
+ }
+ }
+}
+
+method W5(N: real)
+{
+ var i, n := 0.0, N;
+ while i != n
+ {
+ if i < n {
+ i := i + 1.0;
+ if n < i { break; }
+ } else {
+ n := n + 1.0;
+ if i < n { break; }
+ }
+ }
+}
|