1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
import org.why3.majority.Candidate;
import org.why3.majority.Mjrty;
public class MjrtyTest {
public static class Candidate implements org.why3.majority.Candidate {
public boolean equals(org.why3.majority.Candidate other) {
return this == other;
}
}
static void majority(Candidate c, Candidate[] arr) {
assert(c.equals(Mjrty.mjrty(arr)));
}
static void no_majority(Candidate[] arr) {
try {
Mjrty.mjrty(arr);
assert(false);
} catch(org.why3.majority.MjrtyNotFoundException e) {
}
}
public static void main(String[] args) {
Candidate A = new Candidate();
Candidate B = new Candidate();
Candidate C = new Candidate();
assert(A.equals(A));
assert(!A.equals(B));
assert(!A.equals(C));
assert(!B.equals(C));
majority(A, new Candidate[] { A, A });
majority(A, new Candidate[] { A, A, A });
no_majority(new Candidate[] { A, A, A, C, C, B, B });
no_majority(new Candidate[] { A, A, A, C, C, B, B, C, C, C });
majority(C, new Candidate[] { A, A, A, C, C, B, B, C, C, C, B, C, C });
no_majority(new Candidate[] { A, A, A, B, B, B, C });
}
}
|
