diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 16:13:03 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-10 16:13:03 -0700 |
| commit | 045044dca10db5cca9b1127755e2b86568dbd575 (patch) | |
| tree | 842bad7f928977a7ce79ef6f6635f4e399965396 /Test/dafny0/Superposition.dfy | |
| parent | ac3efe8ee031e3e620f06709be2f35c96d022c92 (diff) | |
Dafny: improved checking of inherited postconditions (in refinements)
Diffstat (limited to 'Test/dafny0/Superposition.dfy')
| -rw-r--r-- | Test/dafny0/Superposition.dfy | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/Test/dafny0/Superposition.dfy b/Test/dafny0/Superposition.dfy new file mode 100644 index 00000000..c4e74871 --- /dev/null +++ b/Test/dafny0/Superposition.dfy @@ -0,0 +1,56 @@ +module M0 {
+ class C {
+ method M(c: C, x: int, y: int) returns (r: int)
+ requires 0 <= x && 0 <= y;
+ ensures r < 100;
+ {
+ if (c == null) {
+ assert c == null;
+ } else if (*) {
+ assert 0 <= x;
+ } else {
+ assert 0 <= y;
+ }
+ r := 8;
+ }
+
+ predicate P(x: int)
+ ensures true; // this postcondition will not be re-checked in refinements, because it does not mention P itself (or anything else that may change in the refinement)
+ ensures x < 60 ==> P(x);
+ {
+ true
+ }
+
+ predicate Q(x: int)
+ ensures Q(x) ==> x < 60; // error: postcondition violation
+ {
+ true
+ }
+
+ predicate R(x: int)
+ ensures R(x) ==> x < 60; // error: postcondition violation
+ {
+ true
+ }
+ }
+}
+
+module M1 refines M0 {
+ class C {
+ method M... // no further proof obligations for M, which is just making M0.M more deterministic
+ {
+ if ... {}
+ else if (x == y) {}
+ else {}
+ }
+
+ predicate P... // error: inherited postcondition 'x < 60 ==> P(x)' is violated by this strengthening of P()
+ {
+ false // with this strengthening of P(), the postcondition fails (still, note that only one of the postconditions is re-checked)
+ }
+
+ predicate Q... // we don't want another error about Q's body here (because it should not be re-checked here)
+ // Ditto for R
+ }
+}
+
|