diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 10:02:41 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-20 10:02:41 -0700 |
| commit | a8e619e3e23d5c426ef583411c3ddf223bc26fbe (patch) | |
| tree | 695a85c032069d02cdecbaeb929439e8ca39a058 /Test/triggers | |
| parent | e3fff39c37ed68cf718eab84613e3bbb02858653 (diff) | |
Add a test to show how trigger splitting balances the downsides of loop detection
Diffstat (limited to 'Test/triggers')
| -rw-r--r-- | Test/triggers/splitting-triggers-recovers-expressivity.dfy | 61 | ||||
| -rw-r--r-- | Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect | 10 |
2 files changed, 71 insertions, 0 deletions
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy b/Test/triggers/splitting-triggers-recovers-expressivity.dfy new file mode 100644 index 00000000..79a0dc72 --- /dev/null +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy @@ -0,0 +1,61 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P(i: int)
+predicate Q(i: int)
+
+/* This file demonstrates a case where automatic trigger splitting is useful to
+ prevent loop detection from reducing expressivity too much. */
+
+lemma exists_0()
+ requires P(0)
+ ensures exists i {:split false} :: P(i) || (Q(i) ==> P(i+1)) {
+ // Fails: P(i) is not a trigger
+}
+
+lemma forall_0(i: int)
+ requires forall j {:split false} :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))
+ requires i >= 0
+ ensures P(i) {
+ // Fails: P(i) is not a trigger
+}
+
+
+lemma exists_1()
+ requires P(0)
+ ensures exists i {:split false} :: P(i) || (Q(i) ==> P(i+1)) {
+ assert Q(0) || !Q(0);
+ // Works: the dummy assertion introduces a term that causes the quantifier
+ // to trigger, producing a witness.
+ }
+
+lemma forall_1(i: int)
+ requires forall j {:split false} :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))
+ requires i >= 0
+ ensures P(i) {
+ assert Q(i) || !Q(i);
+ // Works: the dummy assertion introduces a term that causes the quantifier
+ // to trigger, producing a witness.
+}
+
+
+lemma exists_2()
+ requires P(0)
+ ensures exists i :: P(i) || (Q(i) ==> P(i+1)) {
+ // Works: automatic trigger splitting allows P(i) to get its own triggers
+}
+
+lemma forall_2(i: int)
+ requires forall j :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))
+ requires i >= 0
+ ensures P(i) {
+ // Works: automatic trigger splitting allows P(i) to get its own triggers
+}
+
+
+lemma loop()
+ requires P(0)
+ requires forall i {:matchingloop} :: i >= 0 ==> Q(i) && (P(i) ==> P(i+1))
+ ensures P(100) {
+ // Works: the matching loop is explicitly allowed
+}
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect new file mode 100644 index 00000000..8d7ff4ef --- /dev/null +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -0,0 +1,10 @@ +splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.
+splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+splitting-triggers-recovers-expressivity.dfy(19,15): Error BP5003: A postcondition might not hold on this return path.
+splitting-triggers-recovers-expressivity.dfy(19,10): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 14 verified, 2 errors
|