diff options
| author |  rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
| commit | 2e8f477b81b1c5c6d3c3f600abac3874548a9e4d (patch) | |
| tree | 03e89bdb4df3a689b7217c5e913557c5b6c6df99 /Test/dafny1/UltraFilter.dfy | |
| parent | 22e67dc18705c19b617678358c8e859349938ac3 (diff) | |
Boogie:
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
Diffstat (limited to 'Test/dafny1/UltraFilter.dfy')
| -rw-r--r-- | Test/dafny1/UltraFilter.dfy | 108 |
1 files changed, 108 insertions, 0 deletions
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy new file mode 100644 index 00000000..61e86836 --- /dev/null +++ b/Test/dafny1/UltraFilter.dfy @@ -0,0 +1,108 @@ +// ultra filter
+
+class UltraFilter<G> {
+ static function IsFilter(f: set<set<G>>, S: set<G>): bool
+ {
+ (forall A, B :: A in f && A <= B ==> B in f) &&
+ (forall C, D :: C in f && D in f ==> C * D in f) &&
+ S in f &&
+ {} !in f
+ }
+
+ static function IsUltraFilter(f: set<set<G>>, S: set<G>): bool
+ {
+ IsFilter(f, S) &&
+ (forall g :: IsFilter(g, S) && f <= g ==> f == g)
+ }
+
+ method Theorem(f: set<set<G>>, S: set<G>, M: set<G>, N: set<G>)
+ requires IsUltraFilter(f, S);
+ requires M + N in f;
+ ensures M in f || N in f;
+ {
+ if (M !in f) {
+ // instantiate 'g' with the following 'h'
+ call h := H(f, S, M);
+ call Lemma_HIsFilter(h, f, S, M);
+ call Lemma_FHOrdering0(h, f, S, M);
+ }
+ }
+
+ // Dafny currently does not have a set comprehension expression, so this method stub will have to do
+ method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>);
+ ensures (forall X :: X in h <==> M + X in f);
+
+ method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires M !in f;
+ ensures IsFilter(h, S);
+ {
+ // call Lemma_H0(h, f, S, M, *, *);
+ assume (forall A, B :: A in h && A <= B ==> B in h);
+
+ // call Lemma_H1(h, f, S, M, *, *);
+ assume (forall C, D :: C in h && D in h ==> C * D in h);
+
+ call Lemma_H2(h, f, S, M);
+
+ call Lemma_H3(h, f, S, M);
+ }
+
+ method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires A in h && A <= B;
+ ensures B in h;
+ {
+ assert M + A <= M + B;
+ }
+
+ method Lemma_H1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, C: set<G>, D: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires C in h && D in h;
+ ensures C * D in h;
+ {
+ assert (M + C) * (M + D) == M + (C * D);
+ }
+
+ method Lemma_H2(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ ensures S in h;
+ {
+ // S is intended to stand for the universal set, but this is the only place where that plays a role
+ assume M <= S;
+
+ assert M + S == S;
+ }
+
+ method Lemma_H3(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires M !in f;
+ ensures {} !in h;
+ {
+ assert M + {} == M;
+ }
+
+ method Lemma_FHOrdering0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ requires IsFilter(h, S);
+ ensures f <= h;
+ {
+ // call Lemma_FHOrdering1(h, f, S, M, *);
+ assume (forall Y :: Y in f ==> Y in h);
+ assume f <= h; // hickup in boxing
+ }
+
+ method Lemma_FHOrdering1(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, Y: set<G>)
+ requires IsFilter(f, S);
+ requires (forall X :: X in h <==> M + X in f);
+ ensures Y in f ==> Y in h;
+ {
+ assert Y <= M + Y;
+ }
+}
|