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 | 26ebf57c586412ab135304dd6551a525e29a9f35 (patch) | |
| tree | cb49024793384a092bf8533896be0859b77a6b71 /Test/dafny0/Definedness.dfy | |
| parent | 3de673998d9e386da3b7e385f45a1b1c6e252e81 (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;
}
}
|