From a8e619e3e23d5c426ef583411c3ddf223bc26fbe Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 20 Aug 2015 10:02:41 -0700
Subject: Add a test to show how trigger splitting balances the downsides of
 loop detection

---
 .../splitting-triggers-recovers-expressivity.dfy   | 61 ++++++++++++++++++++++
 ...tting-triggers-recovers-expressivity.dfy.expect | 10 ++++
 2 files changed, 71 insertions(+)
 create mode 100644 Test/triggers/splitting-triggers-recovers-expressivity.dfy
 create mode 100644 Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect

(limited to 'Test/triggers')

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
-- 
cgit v1.2.3