summaryrefslogtreecommitdiff
path: root/Test/hofs
diff options
context:
space:
mode:
Diffstat (limited to 'Test/hofs')
-rw-r--r--Test/hofs/ReadsReads.dfy4
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index a6f8d922..60ac35f5 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -105,14 +105,14 @@ module WhatWeKnowAboutReads {
module ReadsAll {
function A(f: int -> int) : int
- reads set o,x | o in f.reads(x) :: o
+ reads set x,o | o in f.reads(x) :: o // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal)
requires forall x :: f.requires(x)
{
f(0) + f(1) + f(2)
}
function method B(f: int -> int) : int
- reads set o,x | o in f.reads(x) :: o
+ reads set x,o | o in f.reads(x) :: o // note, with "set o,x ..." instead, Dafny complains (this is perhaps less than ideal)
requires forall x :: f.requires(x)
{
f(0) + f(1) + f(2)