diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2013-01-18 17:54:04 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2013-01-18 17:54:04 -0800 |
| commit | 472f3de939e7b5d652a0d7b478a3edc1fec17a99 (patch) | |
| tree | 5571c083bac606b31ba5f628ba88bb7543c5057c /Test/dafny0/CoResolution.dfy | |
| parent | 252dfd009b02014037fb154ff744d7644f0e0ab8 (diff) | |
Some additional resolution checks for co stuff.
Beefed up some test cases.
Diffstat (limited to 'Test/dafny0/CoResolution.dfy')
| -rw-r--r-- | Test/dafny0/CoResolution.dfy | 96 |
1 files changed, 64 insertions, 32 deletions
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy index 3146147e..1b1923c3 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -1,38 +1,31 @@ -copredicate P(b: bool)
-{
- !b && Q(null)
-}
-
-copredicate Q(a: array<int>)
-{
- a == null && P(true)
-}
-
-//copredicate A() { B() }
-//predicate B() { A() } // error: SCC of a copredicate must include only copredicates
+module TestModule {
+ copredicate P(b: bool)
+ {
+ !b && Q(null)
+ }
-copredicate D()
- reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
-{
- true
-}
+ copredicate Q(a: array<int>)
+ {
+ a == null && P(true)
+ }
-copredicate S(d: set<int>)
-{
- this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
- Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
- this.S#[5](d) &&
- S#[5](d) &&
- S#[_k](d) // error: _k is not an identifier in scope
-}
+ copredicate S(d: set<int>)
+ {
+ this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
+ Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
+ this.S#[5](d) &&
+ S#[5](d) &&
+ S#[_k](d) // error: _k is not an identifier in scope
+ }
-comethod CM(d: set<int>)
-{
- var b;
- b := this.S#[5](d);
- b := S#[5](d);
- this.CM#[5](d);
- CM#[5](d);
+ comethod CM(d: set<int>)
+ {
+ var b;
+ b := this.S#[5](d);
+ b := S#[5](d);
+ this.CM#[5](d);
+ CM#[5](d);
+ }
}
module GhostCheck0 {
@@ -65,3 +58,42 @@ module GhostCheck2 { }
}
}
+
+module Mojul0 {
+ copredicate D()
+ reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
+ {
+ true
+ }
+
+ copredicate NoEnsuresPlease(m: nat)
+ ensures NoEnsuresPlease(m) ==> m < 100; // error: a copredicate is not allowed to have an 'ensures' clause
+ {
+ m < 75
+ }
+
+ // Note, 'decreases' clauses are also disallowed on copredicates, but the parser takes care of that
+}
+
+module Mojul1 {
+ copredicate A() { B() } // error: SCC of a copredicate must include only copredicates
+ predicate B() { A() }
+
+ copredicate X() { Y() }
+ copredicate Y() { X#[10]() } // error: X is not allowed to depend on X#
+
+ comethod M()
+ {
+ N();
+ }
+ comethod N()
+ {
+ Z();
+ W(); // error: not allowed to make co-recursive call to non-comethod
+ }
+ ghost method Z() { }
+ ghost method W() { M(); }
+
+ comethod G() { H(); }
+ comethod H() { G#[10](); } // fine for comethod/prefix-method
+}
|