diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-27 21:25:06 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-27 21:25:06 -0700 |
commit | 1e725f0c9382a3dd8be109d160581868c9567f61 (patch) | |
tree | 8f4112342c757d402b9e74dbe1b15a6dd3e1001c /Test/triggers/loop-detection-is-not-too-strict.dfy | |
parent | 7a993f6c87eaa82f383b1c5e7411f1878d4edf30 (diff) |
Further relax the loop detection conditions
Mismatches are now allowed up to expressions not involving any of the bound
variables of the quantifier under inspection.
Diffstat (limited to 'Test/triggers/loop-detection-is-not-too-strict.dfy')
-rw-r--r-- | Test/triggers/loop-detection-is-not-too-strict.dfy | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy index a5a30c81..81f764ad 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy @@ -7,8 +7,9 @@ // equal to that trigger, as long as the only differences are variable
predicate P(x: int, y: int)
+predicate Q(x: int)
-method Test() {
+method Test(z: int) {
// P(x, y) and P(y, x) might look like they would cause a loop. Since they
// only differ by their variables, though, they won't raise flags.
assume forall x: int, y: int :: P(x, y) == P(y, x);
@@ -18,4 +19,22 @@ method Test() { // Contrast with the following:
assume forall x: int, y: int :: P(x, y) == P(x, y+1);
+
+ // The following examples were made legal after an exchange where Chris
+ // pointed examples in the IronClad sources where things like this were
+ // incorrectly flagged.
+ assert forall x :: true || Q(x) || Q(0);
+ assert forall x :: true || Q(x) || Q(z);
+ assert forall x :: true || P(x, 1) || P(x, z);
+
+ // Support for the following was added following a discussion with Rustan; in
+ // the second one the expression `if z > 1 then z else 3 * z + 1` is not
+ // directly a constant expression, but it does not involve x, so it's ok:
+ assert forall x :: true || Q(x) || Q(0+1);
+ assert forall x :: true || Q(x) || Q(if z > 1 then z else 3 * z + 1);
+ // Sanity check:
+ assert forall x :: true || Q(x) || Q(if z > 1 then x else 3 * z + 1);
+
+ // WISH: It might also be good to zeta-reduce before loop detection.
+ assert forall x :: true || Q(x) || (var xx := x+1; Q(xx));
}
|