diff options
author | Rustan Leino <leino@microsoft.com> | 2011-05-27 01:19:41 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-05-27 01:19:41 -0700 |
commit | 9a714cafa2e4d6551f28c57187c28333cc155527 (patch) | |
tree | b5ff4040448ecd26ac8482e4dc1227781e38e296 /Test/dafny0/Definedness.dfy | |
parent | e840f558d5079001d222a289c9a14ed82c9573c3 (diff) |
Dafny: retired "use" statements
Diffstat (limited to 'Test/dafny0/Definedness.dfy')
-rw-r--r-- | Test/dafny0/Definedness.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 255b38e3..92ac0793 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -180,12 +180,12 @@ class StatementTwoShoes { method V(s: set<StatementTwoShoes>, a: int, b: int)
modifies s;
{
- use G(12 / b); // fine, because there are no welldefinedness checks on use statements
+
foreach (m in s | m.x < 200) // s may contain null, but the foreach excludes null
{
assume 0 <= m.x;
assert m.x < 1000;
- use G(5 / m.x); // fine, because there are no welldefinedness checks on use statements
+
m.x := m.x + 1;
}
foreach (m in s + {F(a)}) // error: collection expression may not be well defined (fn precondition)
|