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/hofs/Classes.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/hofs/Classes.dfy')
-rw-r--r-- | Test/hofs/Classes.dfy | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy index 2b892b35..0ceb46f1 100644 --- a/Test/hofs/Classes.dfy +++ b/Test/hofs/Classes.dfy @@ -30,15 +30,14 @@ function B(t : T) : int -> int } function J(t : T) : int - requires t != null; - requires t.h.reads(0) == {}; - reads t; - reads if t != null then t.h.reads(0) else {}; + requires t != null + reads t + reads t.h.reads(0) { if t.h.requires(0) then B(t)(0) else - B(t)(0) // fail + B(t)(0) // error: precondition violation } method U(t : T) |