diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-02-08 15:33:23 +0100 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-02-08 15:33:23 +0100 |
| commit | 6a73bfff8499eb7a128de01c20488a9f53e397c7 (patch) | |
| tree | 1958510741be38d9972453b2ad42ab265270fb43 /Test/dafny2 | |
| parent | bc0e2a5f6ef893c549c3a244faa17e7f235a2de0 (diff) | |
Changed calc syntax (custom operators are now written before the hint)
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/MajorityVote.dfy | 14 |
1 files changed, 8 insertions, 6 deletions
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);
}
|