diff options
| author |  rustanleino <unknown> | 2010-03-12 04:12:37 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-12 04:12:37 +0000 |
| commit | e0a48b3b117393f7926c5723eb789db4fdea3267 (patch) | |
| tree | 989eb590dd1d799c3a48bc4334426986af688d8d /Test/dafny0 | |
| parent | b412ff49609070ff67da19eac90bf9d85b0c096f (diff) | |
Dafny:
* Modifies clause checking is now done with each update, instead of at the end of the method. Not only does this improve error messages, but on some examples, it gives a dramatic speed-up (2x) in proving time.
* bugfix: range expressions of foreach statements were previously ignored during Translation
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 20 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 84 |
2 files changed, 103 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 1edbeedc..d46dc7fe 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -98,8 +98,26 @@ Execution trace: (0,0): anon3
(0,0): anon11_Then
(0,0): anon6
+SmallTests.dfy(95,5): Error: call may violate caller's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+ (0,0): anon3
+SmallTests.dfy(108,7): Error: call may violate caller's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+SmallTests.dfy(110,7): Error: call may violate caller's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+SmallTests.dfy(150,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+ (0,0): anon3
-Dafny program verifier finished with 6 verified, 4 errors
+Dafny program verifier finished with 10 verified, 8 errors
-------------------- Queue.dfy --------------------
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 6ac9879d..3a2ca13c 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -67,3 +67,87 @@ class Node { 12
}
}
+
+// ------------------ modifies clause tests ------------------------
+
+class Modifies {
+ var x: int;
+ var next: Modifies;
+
+ method A(p: Modifies)
+ modifies this, p;
+ {
+ x := x + 1;
+ while (p != null && p.x < 75)
+ decreases 75 - p.x;
+ {
+ p.x := p.x + 1;
+ }
+ }
+
+ method B(p: Modifies)
+ modifies this;
+ {
+ call A(this);
+ if (p == this) {
+ call p.A(p);
+ }
+ call A(p); // error: may violate modifies clause
+ }
+
+ method C(b: bool)
+ modifies this;
+ ensures !b ==> x == old(x) && next == old(next);
+ {
+ }
+
+ method D(p: Modifies, y: int)
+ requires p != null;
+ {
+ if (y == 3) {
+ call p.C(true); // error: may violate modifies clause
+ } else {
+ call p.C(false); // error: may violation modifies clause (the check is done without regard
+ // for the postcondition, which also makes sense, since there may, in
+ // principle, be other fields of the object that are not constrained by the
+ // postcondition)
+ }
+ }
+
+ method E()
+ modifies this;
+ {
+ call A(null); // allowed
+ }
+
+ method F(s: set<Modifies>)
+ modifies s;
+ {
+ foreach (m in s | 2 <= m.x) {
+ m.x := m.x + 1;
+ }
+ if (this in s) {
+ x := 2 * x;
+ }
+ }
+
+ method G(s: set<Modifies>)
+ modifies this;
+ {
+ var m := 3; // this is a different m
+
+ foreach (m in s | m == this) {
+ m.x := m.x + 1;
+ }
+ if (s <= {this}) {
+ foreach (m in s) {
+ m.x := m.x + 1;
+ }
+ call F(s);
+ }
+ foreach (m in s) {
+ assert m.x < m.x + 10; // nothing wrong with asserting something
+ m.x := m.x + 1; // error: may violate modifies clause
+ }
+ }
+}
|