diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Calculations.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny2/MajorityVote.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny3/CalcExample.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny3/Dijkstra.dfy | 4 |
4 files changed, 14 insertions, 12 deletions
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy index 9e44f62e..80775896 100644 --- a/Test/dafny0/Calculations.dfy +++ b/Test/dafny0/Calculations.dfy @@ -12,8 +12,8 @@ method CalcTest0(s: seq<int>) { if (|s| > 0) { calc { s[0]; // OK: well-formed in this context - { assert s[0] == s[0]; } - <= s[0]; + <= { assert s[0] == s[0]; } + s[0]; } } } diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy index 1caffe0c..eb7ae766 100644 --- a/Test/dafny2/MajorityVote.dfy +++ b/Test/dafny2/MajorityVote.dfy @@ -239,8 +239,9 @@ method FindWinner'<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns 2 * Count(a, up, |a|, K);
{ Lemma_Split(a, lo, up, |a|, K); }
2 * Count(a, lo, |a|, K) - 2 * Count(a, lo, up, K);
- { assert HasMajority(a, lo, |a|, K); } // loop invariant (1)
- > |a| - lo - 2 * Count(a, lo, up, K);
+ > { assert HasMajority(a, lo, |a|, K); } // loop invariant (1)
+ |a| - lo - 2 * Count(a, lo, up, K);
+ >=
{ if (k == K) {
calc {
2 * Count(a, lo, up, K);
@@ -251,15 +252,15 @@ method FindWinner'<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns } else {
calc {
2 * Count(a, lo, up, K);
- { Lemma_Unique(a, lo, up, k, K); }
- <= 2 * ((up - lo) - Count(a, lo, up, k));
+ <= { Lemma_Unique(a, lo, up, k, K); }
+ 2 * ((up - lo) - Count(a, lo, up, k));
{ assert 2 * Count(a, lo, up, k) == up - lo; } // k has 50% among a[lo..up]
up - lo;
}
}
assert 2 * Count(a, lo, up, K) <= up - lo;
}
- >= |a| - lo - (up - lo);
+ |a| - lo - (up - lo);
|a| - up;
}
assert HasMajority(a, up, |a|, K);
@@ -323,6 +324,7 @@ method FindWinner''<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) return 2 * Count(a, lo, |a|, K) > |a| - lo;
{ Lemma_Split(a, lo, up, |a|, K); }
2 * Count(a, lo, up, K) + 2 * Count(a, up, |a|, K) > |a| - lo;
+ ==>
{ if (k == K) {
calc {
2 * Count(a, lo, up, K);
@@ -343,7 +345,7 @@ method FindWinner''<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) return assert 2 * Count(a, lo, up, K) <= up - lo;
}
// subtract off Count(a, lo, up, K) from the LHS and subtract off the larger amount up - lo from the RHS
- ==> 2 * Count(a, up, |a|, K) > (|a| - lo) - (up - lo);
+ 2 * Count(a, up, |a|, K) > (|a| - lo) - (up - lo);
2 * Count(a, up, |a|, K) > |a| - up;
HasMajority(a, up, |a|, K);
}
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);
|