diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-26 00:02:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-26 00:02:57 -0700 |
| commit | d9f2a82a417703f3669ba8399dcc8bcf34c3d742 (patch) | |
| tree | 08b309fd809639a62c453c33dac86845dd4b9815 /Test/dafny1/UltraFilter.dfy | |
| parent | e52270deab6d2fd5b885848211c2d9d1ab814b09 (diff) | |
Dafny: retired the "call" keyword
Diffstat (limited to 'Test/dafny1/UltraFilter.dfy')
| -rw-r--r-- | Test/dafny1/UltraFilter.dfy | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index 61e86836..189ff2b5 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -22,9 +22,9 @@ class UltraFilter<G> { {
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);
+ var h := H(f, S, M);
+ Lemma_HIsFilter(h, f, S, M);
+ Lemma_FHOrdering0(h, f, S, M);
}
}
@@ -44,9 +44,9 @@ class UltraFilter<G> { // 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);
+ Lemma_H2(h, f, S, M);
- call Lemma_H3(h, f, S, M);
+ 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>)
|