diff options
author | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 18:44:52 -0700 |
---|---|---|
committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-15 18:44:52 -0700 |
commit | e9de4cbd947adfe63c13e771f048a8c392035bb2 (patch) | |
tree | 37a3649653dcada974d39091fd95417dee662fb6 /Test/dafny2 | |
parent | 1512286c445a2aa63649e1501c38690c499e8113 (diff) |
Dafny: support assign-such-that in var declarations in refinements
Diffstat (limited to 'Test/dafny2')
-rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy index 1357b65c..ea26a234 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -18,7 +18,7 @@ module A imports Library { ensures Contents == old(Contents);
ensures thing in Contents && Function.Apply(matchCriterion, thing);
{
- var k; assume k in Contents && Function.Apply(matchCriterion, k);
+ var k :| k in Contents && Function.Apply(matchCriterion, k);
thing := k;
}
}
@@ -49,7 +49,7 @@ module B refines A { if (Function.Apply(matchCriterion, arr[i])) { break; }
i := i + 1;
}
- var k := arr[i]; assert ...;
+ var k := arr[i];
}
}
}
|