diff options
author | Rustan Leino <unknown> | 2015-06-15 17:00:04 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2015-06-15 17:00:04 -0700 |
commit | cc0a7cae53c068993e3b3004049629dd396cb649 (patch) | |
tree | bb1ae056cded89fdcddcd84294d6accc4c9d03ac /Test/dafny0/Reads.dfy | |
parent | 58d639bff25a2d4dadf6febb81b1438e957c43cd (diff) |
Changed logical order of requires and reads clauses on functions. Reads clauses
can now assume the precondition (as had also been the case back in the days when
reads clauses had to be self framing).
Diffstat (limited to 'Test/dafny0/Reads.dfy')
-rw-r--r-- | Test/dafny0/Reads.dfy | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy index 7e0ca1c4..6dedbada 100644 --- a/Test/dafny0/Reads.dfy +++ b/Test/dafny0/Reads.dfy @@ -58,7 +58,7 @@ function ok5(r : R):() // Reads checking where there are circularities among the expressions class CircularChecking { - var Repr: set<object> + ghost var Repr: set<object> function F(): int reads this, Repr @@ -76,8 +76,8 @@ class CircularChecking { requires Repr == {} function H0(cell: Cell): int - reads Repr // error: reads is not self-framing (unless "this in Repr") - requires this in Repr // lo and behold! So, reads clause is fine, if we can assume the precondition + reads Repr // by itself, this reads is not self-framing + requires this in Repr // lo and behold! So, reads clause is fine after all function H1(cell: Cell): int reads this, Repr @@ -126,3 +126,13 @@ function FunctionInQuantifier2(): int var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100; // fine :) :) f(10) } + +class DynamicFramesIdiom { + ghost var Repr: set<object> + predicate IllFormed_Valid() + reads Repr // error: reads is not self framing (notice the absence of "this") + { + this in Repr // this says that the predicate returns true if "this in Repr", but the + // predicate can also be invoked in a state where its body will evaluate to false + } +} |