diff options
author | 2010-06-11 02:02:36 +0000 | |
---|---|---|
committer | 2010-06-11 02:02:36 +0000 | |
commit | d0411d08eba6e800509744dbb9e0b4c380964e9b (patch) | |
tree | b67726e5eb114d28fc8af048344f16ed8eed71bd /Test/dafny0/Definedness.dfy | |
parent | 5dddcccf78dbd7752963c5fe9da288697ccd27eb (diff) |
Dafny: Added two additional heuristics for guessing missing loop decreases clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
Diffstat (limited to 'Test/dafny0/Definedness.dfy')
-rw-r--r-- | Test/dafny0/Definedness.dfy | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index b69fa4f6..d557de21 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -161,14 +161,12 @@ class StatementTwoShoes { var i := 0;
while (i < 100)
invariant i <= 100;
- decreases 100 - i;
invariant F(123 - i) == this;
{
i := i + 1;
}
i := 0;
while (i < 100)
- decreases 100 - i;
invariant F(if i==77 then -3 else i) == this; // error: expression may not be well defined
{
i := i + 1;
@@ -210,7 +208,6 @@ class StatementTwoShoes { while (i < 100)
// The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking
invariant 5 / x != 5 / x; // error: not well-defined, and error: loop invariant does not hold initially
- decreases 100 - i;
{
i := i + 1;
}
|