diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-28 18:51:27 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-28 18:51:27 -0700 |
| commit | 7b8adafdc184fd812fbb26d4d4ca4aaf5f0d134a (patch) | |
| tree | 727566ae9586fa19d32c71b3872a57392ce9cd0f /Test/dafny0/Definedness.dfy | |
| parent | 7cf0e87a3c9cbc769a9248604e8943a7faddd914 (diff) | |
Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"
Diffstat (limited to 'Test/dafny0/Definedness.dfy')
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 92ac0793..8df1a7c5 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -151,7 +151,7 @@ class StatementTwoShoes { while (20 / k == 5 && j < 100) // error: guard may not be well defined (div by zero)
decreases 100 - j;
{
- havoc k;
+ k := *;
j := j + 1;
}
}
|