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 | |
| 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')
| -rw-r--r-- | Test/dafny0/Answer | 8 | ||||
| -rw-r--r-- | Test/dafny0/CoResolution.dfy | 62 |
2 files changed, 69 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c79d166a..b462465d 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1242,7 +1242,13 @@ CoResolution.dfy(70,31): Error: a copredicate is not allowed to declare any ensu CoResolution.dfy(79,20): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(83,20): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to other comethods and prefix methods
-10 resolution/type errors detected in CoResolution.dfy
+CoResolution.dfy(106,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods
+CoResolution.dfy(107,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods
+CoResolution.dfy(126,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods
+CoResolution.dfy(127,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods
+CoResolution.dfy(146,4): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(148,4): Error: a recursive call from a copredicate can go only to other copredicates
+16 resolution/type errors detected in CoResolution.dfy
-------------------- CoPrefix.dfy --------------------
CoPrefix.dfy(161,3): Error BP5003: A postcondition might not hold on this return path.
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
+ }
+}
|