diff options
| author |  Rustan Leino <unknown> | 2013-08-04 18:38:50 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-04 18:38:50 -0700 |
| commit | ebbb5597c34d69490704b7425cf80830b8e99f7e (patch) | |
| tree | 9c049807a267e4ea0df3e3cd6e1a39f89be4600a /Test/dafny0/CoResolution.dfy | |
| parent | a1710a324a8d92935cd7bc8ecbda115b9cd09748 (diff) | |
Disallow call-graph clusters that mix co-methods / prefix methods with other things.
Disallow call-graph clusters that mix co-predicates / prefix predicates with other things.
Diffstat (limited to 'Test/dafny0/CoResolution.dfy')
| -rw-r--r-- | Test/dafny0/CoResolution.dfy | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy index 1b1923c3..9ab52d53 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -97,3 +97,65 @@ module Mojul1 { comethod G() { H(); }
comethod H() { G#[10](); } // fine for comethod/prefix-method
}
+
+module CallGraph {
+ // comethod -> copredicate -> comethod
+ // comethod -> copredicate -> prefix method
+ comethod CoLemma(n: nat)
+ {
+ var q := Q(n); // error
+ var r := R(n); // error
+ }
+
+ copredicate Q(n: nat)
+ {
+ calc { 87; { CoLemma(n); } }
+ false
+ }
+
+ copredicate R(n: nat)
+ {
+ calc { 87; { CoLemma#[n](n); } }
+ false
+ }
+
+ // comethod -> prefix predicate -> comethod
+ // comethod -> prefix predicate -> prefix method
+ comethod CoLemma_D(n: nat)
+ {
+ var q := Q_D#[n](n); // error
+ var r := R_D#[n](n); // error
+ }
+
+ copredicate Q_D(n: nat)
+ {
+ calc { 88; { CoLemma_D(n); } }
+ false
+ }
+
+ copredicate R_D(n: nat)
+ {
+ calc { 89; { CoLemma_D#[n](n); } }
+ false
+ }
+
+ // copredicate -> function -> copredicate
+ // copredicate -> function -> prefix predicate
+ copredicate P(n: nat)
+ {
+ G0(n) // error
+ <
+ G1(n) // error
+ }
+
+ function G0(n: nat): int
+ {
+ calc { true; { assert P(n); } }
+ 100
+ }
+ function G1(n: nat): int
+ {
+ calc { true; { assert P#[n](n); } }
+ 101
+ }
+}
|