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 | e1bf8c0bfff274a0651fb581951cfcaae8b34007 (patch) | |
| tree | 03754af126357448a0c055a50a90c98879966a40 /Test/dafny0/Definedness.dfy | |
| parent | 0de8c9463a1e948fd11d9fe34c729f26b3e1af1b (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)
|