From b8b483f2529746a2fee7378b2fabb8dcf3e048fd Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 19 Oct 2012 16:45:57 -0700 Subject: added two "calc" proofs (by Nadia) of the MajorityVote example --- Test/dafny2/Answer | 2 +- Test/dafny2/Calculations.dfy | 4 +- Test/dafny2/MajorityVote.dfy | 182 ++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 184 insertions(+), 4 deletions(-) (limited to 'Test/dafny2') diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 2feaf6f7..d83c766c 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -45,7 +45,7 @@ Dafny program verifier finished with 3 verified, 0 errors -------------------- MajorityVote.dfy -------------------- -Dafny program verifier finished with 11 verified, 0 errors +Dafny program verifier finished with 16 verified, 0 errors -------------------- SegmentSum.dfy -------------------- diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 8c13457b..19e0645f 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -80,7 +80,7 @@ ghost method Lemma_Revacc_calc(xs: List, ys: List) concat(revacc(xrest, Cons(x, Nil)), ys); { Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs) revacc(xrest, concat(Cons(x, Nil), ys)); - // def. concat (x2) + // def. concat (x2) revacc(xrest, Cons(x, ys)); // def. revacc revacc(xs, ys); @@ -115,7 +115,7 @@ ghost method Lemma_Revacc(xs: List, ys: List) assert concat(reverse(xs), ys) == // def. reverse concat(concat(reverse(xrest), Cons(x, Nil)), ys) - == // induction hypothesis: Lemma3a(xrest, Cons(x, Nil)) + == // induction hypothesis: Lemma_Revacc(xrest, Cons(x, Nil)) concat(revacc(xrest, Cons(x, Nil)), ys); Lemma_RevCatCommute(); // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs) assert concat(revacc(xrest, Cons(x, Nil)), ys) diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy index af67ee92..1caffe0c 100644 --- a/Test/dafny2/MajorityVote.dfy +++ b/Test/dafny2/MajorityVote.dfy @@ -51,6 +51,14 @@ // to the Count function. Alternatively, one could have added the antecedent "c in a" or // "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection. +// About reading the proofs: +// Dafny proves the FindWinner algorithm from the given loop invariants and the two lemmas +// Lemma_Unique and Lemma_Split. In showing this proof to some colleagues, they found they +// were not as quick as Dafny in constructing the proof from these ingredients. For a human +// to understand the situation better, it helps to take smaller (and more) steps in the proof. +// At the end of this file, Nadia Polikarpova has written two versions of FindWinner that does +// that, using Dafny's support for calculational proofs. + function method Count(a: seq, s: int, t: int, x: T): int requires 0 <= s <= t <= |a|; ensures Count(a, s, t, x) == 0 || x in a; @@ -59,10 +67,16 @@ function method Count(a: seq, s: int, t: int, x: T): int Count(a, s, t-1, x) + if a[t-1] == x then 1 else 0 } +predicate HasMajority(a: seq, s: int, t: int, x: T) + requires 0 <= s <= t <= |a|; +{ + 2 * Count(a, s, t, x) > t - s +} + // Here is the first version of the algorithm, the one that assumes there is a majority choice. method FindWinner(a: seq, ghost K: Candidate) returns (k: Candidate) - requires 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes + requires HasMajority(a, 0, |a|, K); // K has a (strict) majority of the votes ensures k == K; // find K { k := a[0]; @@ -173,3 +187,169 @@ ghost method Lemma_Unique(a: seq, s: int, t: int, x: T, y: T) } */ } + +// ------------------------------------------------------------------------------ + +// This version uses more calculations with integer formulas +method FindWinner'(a: seq, ghost K: Candidate) returns (k: Candidate) + requires HasMajority(a, 0, |a|, K); // K has a (strict) majority of the votes + ensures k == K; // find K +{ + k := a[0]; // Current candidate: the first element + var lo, up, c := 0, 1, 1; // Window: [0..1], number of occurrences of k in the window: 1 + while (up < |a|) + invariant 0 <= lo < up <= |a|; // (0) + invariant HasMajority(a, lo, |a|, K); // (1) K has majority among a[lo..] + invariant HasMajority(a, lo, up, k); // (2) k has majority among a[lo..up] (in the current window) + invariant c == Count(a, lo, up, k); // (3) + { + if (a[up] == k) { + // One more occurrence of k + up, c := up + 1, c + 1; + } else if (2 * c > up + 1 - lo) { + // An occurrence of another value, but k still has the majority + up := up + 1; + } else { + // An occurrence of another value and k just lost the majority. + // Prove that k has exactly 50% in the future window a[lo..up + 1]: + calc /* k has 50% among a[lo..up + 1] */ { + true; + // negation of the previous branch condition; + 2 * c <= up + 1 - lo; + // loop invariant (3) + 2 * Count(a, lo, up, k) <= up + 1 - lo; + calc { + true; + // loop invariant (2) + HasMajority(a, lo, up, k); + // def. HasMajority + 2 * Count(a, lo, up, k) > up - lo; + 2 * Count(a, lo, up, k) >= up + 1 - lo; + } + 2 * Count(a, lo, up, k) == up + 1 - lo; + } + up := up + 1; + assert 2 * Count(a, lo, up, k) == up - lo; // k has exactly 50% in the current window a[lo..up] + + // We are going to start a new window a[up..up + 1] and choose a new candidate, + // so invariants (2) and (3) will be easy to re-establish. + // To re-establish (1) we have to prove that K has majority among a[up..], as up will become the new lo. + // The main idea is that we had enough K's in a[lo..], and there cannot be too many in a[lo..up]. + calc /* K has majority among a[up..] */ { + 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); + { if (k == K) { + calc { + 2 * Count(a, lo, up, K); + 2 * Count(a, lo, up, k); + { assert 2 * Count(a, lo, up, k) == up - lo; } // k has 50% among a[lo..up] + up - lo; + } + } else { + calc { + 2 * 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| - up; + } + assert HasMajority(a, up, |a|, K); + + k, lo, up, c := a[up], up, up + 1, 1; + assert HasMajority(a, lo, |a|, K); + } + } + Lemma_Unique(a, lo, |a|, K, k); // both k and K have a majority among a[lo..], so K == k +} + +// This version uses more calculations with boolean formulas +method FindWinner''(a: seq, ghost K: Candidate) returns (k: Candidate) + requires HasMajority(a, 0, |a|, K); // K has a (strict) majority of the votes + ensures k == K; // find K +{ + k := a[0]; // Current candidate: the first element + var lo, up, c := 0, 1, 1; // Window: [0..1], number of occurrences of k in the window: 1 + while (up < |a|) + invariant 0 <= lo < up <= |a|; // (0) + invariant HasMajority(a, lo, |a|, K); // (1) K has majority among a[lo..] + invariant HasMajority(a, lo, up, k); // (2) k has majority among a[lo..up] (in the current window) + invariant c == Count(a, lo, up, k); // (3) + { + if (a[up] == k) { + // One more occurrence of k + up, c := up + 1, c + 1; + } else if (2 * c > up + 1 - lo) { + // An occurrence of another value, but k still has the majority + up := up + 1; + } else { + // An occurrence of another value and k just lost the majority. + // Prove that k has exactly 50% in the future window a[lo..up + 1]: + calc /* k has 50% among a[lo..up + 1] */ { + true; + // negation of the previous branch condition; + 2 * c <= up + 1 - lo; + // loop invariant (3) + 2 * Count(a, lo, up, k) <= up + 1 - lo; + calc { + true; + // loop invariant (2) + HasMajority(a, lo, up, k); + // def. HasMajority + 2 * Count(a, lo, up, k) > up - lo; + 2 * Count(a, lo, up, k) >= up + 1 - lo; + } + 2 * Count(a, lo, up, k) == up + 1 - lo; + } + up := up + 1; + assert 2 * Count(a, lo, up, k) == up - lo; // k has exactly 50% in the current window a[lo..up] + + // We are going to start a new window a[up..up + 1] and choose a new candidate, + // so invariants (2) and (3) will be easy to re-establish. + // To re-establish (1) we have to prove that K has majority among a[up..], as up will become the new lo. + // The main idea is that we had enough K's in a[lo..], and there cannot be too many in a[lo..up]. + calc /* K has majority among a[up..] */ { + true; + // loop invariant (1) + HasMajority(a, lo, |a|, K); + 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); + 2 * Count(a, lo, up, k); + { assert 2 * Count(a, lo, up, k) == up - lo; } // k has 50% among a[lo..up] + up - lo; + } + } else { + calc { + true; + { Lemma_Unique(a, lo, up, k, K); } + Count(a, lo, up, K) + Count(a, lo, up, k) <= up - lo; + 2 * Count(a, lo, up, K) + 2 * Count(a, lo, up, k) <= 2 * (up - lo); + { assert 2 * Count(a, lo, up, k) == up - lo; } // k has 50% among a[lo..up] + 2 * Count(a, lo, up, K) <= up - lo; + } + } + 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| - up; + HasMajority(a, up, |a|, K); + } + k, lo, up, c := a[up], up, up + 1, 1; + assert HasMajority(a, lo, |a|, K); + } + } + Lemma_Unique(a, lo, |a|, K, k); // both k and K have a majority among a[lo..], so K == k +} -- cgit v1.2.3