summaryrefslogtreecommitdiff
path: root/Test/dafny3
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny3')
-rw-r--r--Test/dafny3/CalcExample.dfy4
-rw-r--r--Test/dafny3/Dijkstra.dfy4
2 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index c94c18d2..dcd41077 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -19,8 +19,8 @@ method M(a: int, b: int, c: int, x: int)
f(f(a, b), c);
{ assert f(a, b) == x; }
f(x, c);
- { assert c <= x; Monotonicity(c, x); }
- <= f(x, x);
+ <= { assert c <= x; Monotonicity(c, x); }
+ f(x, x);
{ DiagonalIdentity(x); }
x;
}
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index d3ff244a..7497618c 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -28,8 +28,8 @@ ghost method lemma_ping(j: nat, n: nat)
j <= n;
{ lemma_ping(j - 1, n - 1); }
j - 1 <= f(n - 1);
- { lemma_ping(j - 1, f(n - 1)); }
- ==> j - 1 <= f(f(n - 1));
+ ==> { lemma_ping(j - 1, f(n - 1)); }
+ j - 1 <= f(f(n - 1));
// (0)
j - 1 <= f(f(n - 1)) && f(f(n - 1)) < f(n);
==> j - 1 < f(n);