diff options
Diffstat (limited to 'Test/hofs')
-rw-r--r-- | Test/hofs/ReadsReads.dfy | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy index d0a8b43b..3fb03fda 100644 --- a/Test/hofs/ReadsReads.dfy +++ b/Test/hofs/ReadsReads.dfy @@ -131,3 +131,14 @@ module ReadsAll { f(0) + f(1) + f(2) } } + +module ReadsOnFunctions { + lemma M0(f: int -> int) + { + var g := f.requires; + assert g.reads(10) == f.reads(10); + } +// function F(f: int -> int): int +// requires forall x :: f.reads(x) == {} // should always be allowed to invoke .reads, even if F has an empty reads clause +// { 0 } +} |