diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
commit | e67c951ad9c5c637e36a6f025ba3d6e3ad945416 (patch) | |
tree | 0cfb5c339602e4bdebf4bf97f3f0ccc3923c14d1 /Test/dafny4/set-compr.dfy | |
parent | 000aa762e1fee4b9bd83ec3d7c8b61fd203e2c9d (diff) | |
parent | df5c5f547990c1f80ab7594a1f9287ee03a61754 (diff) |
Merge commit 'df5c5f5'
Diffstat (limited to 'Test/dafny4/set-compr.dfy')
-rw-r--r-- | Test/dafny4/set-compr.dfy | 54 |
1 files changed, 41 insertions, 13 deletions
diff --git a/Test/dafny4/set-compr.dfy b/Test/dafny4/set-compr.dfy index 71a07f3d..d093a924 100644 --- a/Test/dafny4/set-compr.dfy +++ b/Test/dafny4/set-compr.dfy @@ -22,7 +22,7 @@ method O() returns (ghost p: set<object>) method P() returns (p: set<object>)
{
- p := set o: object | true; // not allowed -- not in a ghost context
+ p := set o: object | true; // error: not (easily) compilable
}
ghost method Q() returns (p: set<object>)
@@ -30,26 +30,54 @@ ghost method Q() returns (p: set<object>) p := set o: object | true; // allowed, since the whole method is ghost
}
-function F(): int
+function F(p: object): int
+ requires p in set o: object | true // error: function is not allowed to depend on allocation state
+ ensures p in set o: object | true // error: ditto (although one could argue that this would be okay)
+ reads set o: object | true // error: same as for 'requires'
+ decreases set o: object | true // error: same as for 'ensures'
+{
+ if p in set o: object | true then // error: function is not allowed to depend on allocation state
+ F(p)
+ else
+ 0
+}
+
+function method G(p: object): int
+ requires p in set o: object | true // error (see F)
+ ensures p in set o: object | true // error (see F)
+ reads set o: object | true // error (see F)
+ decreases set o: object | true // error (see F)
+{
+ if p in set o: object | true then // error (see F)
+ G(p)
+ else
+ 0
+}
+
+method M0() returns (ghost r: int, s: int)
requires null in set o: object | true // allowed
ensures null in set o: object | true // allowed
- reads set o: object | true // allowed
+ modifies set o: object | true // allowed
decreases set o: object | true // allowed
{
- if null in set o: object | true then // allowed -- in a ghost context
- F()
- else
- 0
+ if null in set o: object | true { // this makes the "if" a ghost
+ r := G(null);
+ s := G(null); // error: assignment of non-ghost not allowed inside ghost "if"
+ } else {
+ r := 0;
+ }
}
-function method G(): int
+method M1() returns (ghost r: int, s: int)
requires null in set o: object | true // (X) allowed
ensures null in set o: object | true // (X) allowed
- reads set o: object | true // allowed
+ modifies set o: object | true // allowed
decreases set o: object | true // (X) allowed
{
- if null in set o: object | true then // not allowed, since this is not a ghost context
- G()
- else
- 0
+ if null in set o: object | true { // this makes the "if" a ghost
+ r := G(null);
+ s := G(null); // error: assignment of non-ghost not allowed inside ghost "if"
+ } else {
+ r := 0;
+ }
}
|