Add one more test for induction triggers

Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/induction-triggers.dfy

@@ -0,0 +1,37 @@
+// RUN: %verify --show-hints "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate f(n: nat) { if n == 0 then true else f(n-1) }
+predicate g(n: nat) { false }
+
+// Default: auto-generated trigger ⇒ Proof passes.
+lemma Default(n: nat) ensures f(n) {}
+
+// Manual list of variables ⇒ Proof passes.
+lemma {:induction n} ListOfVars(n: nat) ensures f(n) {}
+
+// No induction ⇒ Proof fails.
+lemma {:induction false} NoInduction(n: nat) ensures f(n) {}
+
+// No induction, with manual proof ⇒ Proof passes.
+lemma {:induction false} ManualInduction(n: nat)
+  ensures f(n)
+{
+  forall ih_n: nat | (n decreases to ih_n) {
+    ManualInduction(ih_n);
+  }
+}
+
+// No triggers, so no auto induction ⇒ Proof fails.
+lemma NoTriggers(n: nat) ensures f(n + 0) {}
+
+// No triggers but forced induction, so warning ⇒ Proof passes.
+lemma {:induction} InductionWarning(n: nat) ensures f(n + 0) {}
+
+// Explicit triggers, so no warning ⇒ Proof passes.
+lemma {:induction} {:inductionTrigger f(n)} NoWarning2(n: nat) ensures f(n + 0) {}
+
+// Legacy mode: auto induction with no triggers ⇒ Proof passes.
+lemma {:inductionTrigger} Legacy(n: nat) ensures f(n) {}
+lemma {:inductionTrigger} Legacy1(n: nat) ensures f(n + 0) {}
+lemma {:induction} {:inductionTrigger} Legacy2(n: nat) ensures f(n + 0) {}

Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/induction-triggers.dfy.expect

@@ -0,0 +1,112 @@
+induction-triggers.dfy(4,10): Info: tail recursive
+  |
+4 | predicate f(n: nat) { if n == 0 then true else f(n-1) }
+  |           ^
+
+induction-triggers.dfy(20,2): Info: Selected triggers: {f(ih_n)}
+   |
+20 |   forall ih_n: nat | (n decreases to ih_n) {
+   |   ^^^^^^
+
+induction-triggers.dfy(4,10): Info: decreases n
+  |
+4 | predicate f(n: nat) { if n == 0 then true else f(n-1) }
+  |           ^
+
+induction-triggers.dfy(17,25): Info: decreases n
+   |
+17 | lemma {:induction false} ManualInduction(n: nat)
+   |                          ^^^^^^^^^^^^^^^
+
+induction-triggers.dfy(8,6): Info: {:induction n}
+  |
+8 | lemma Default(n: nat) ensures f(n) {}
+  |       ^^^^^^^
+
+induction-triggers.dfy(8,6): Info: {:inductionTrigger n}
+  |
+8 | lemma Default(n: nat) ensures f(n) {}
+  |       ^^^^^^^
+
+induction-triggers.dfy(11,21): Info: {:inductionTrigger f(n)}
+   |
+11 | lemma {:induction n} ListOfVars(n: nat) ensures f(n) {}
+   |                      ^^^^^^^^^^
+
+induction-triggers.dfy(26,6): Info: omitting automatic induction (for induction-variable candidate n) because of lack of triggers
+   |
+26 | lemma NoTriggers(n: nat) ensures f(n + 0) {}
+   |       ^^^^^^^^^^
+
+induction-triggers.dfy(29,19): Warning: Could not find a trigger for the induction hypothesis. Without a trigger, this may cause brittle verification. Change or remove the {:induction} attribute to generate a different induction hypothesis, or add {:nowarn} to silence this warning. For more information, see the section quantifier instantiation rules in the reference manual.
+   |
+29 | lemma {:induction} InductionWarning(n: nat) ensures f(n + 0) {}
+   |                    ^^^^^^^^^^^^^^^^
+
+induction-triggers.dfy(29,19): Info: {:induction n}
+   |
+29 | lemma {:induction} InductionWarning(n: nat) ensures f(n + 0) {}
+   |                    ^^^^^^^^^^^^^^^^
+
+induction-triggers.dfy(32,44): Info: {:induction n}
+   |
+32 | lemma {:induction} {:inductionTrigger f(n)} NoWarning2(n: nat) ensures f(n + 0) {}
+   |                                             ^^^^^^^^^^
+
+induction-triggers.dfy(32,44): Info: {:inductionTrigger n}
+   |
+32 | lemma {:induction} {:inductionTrigger f(n)} NoWarning2(n: nat) ensures f(n + 0) {}
+   |                                             ^^^^^^^^^^
+
+induction-triggers.dfy(35,26): Info: {:induction n}
+   |
+35 | lemma {:inductionTrigger} Legacy(n: nat) ensures f(n) {}
+   |                           ^^^^^^
+
+induction-triggers.dfy(36,26): Info: {:induction n}
+   |
+36 | lemma {:inductionTrigger} Legacy1(n: nat) ensures f(n + 0) {}
+   |                           ^^^^^^^
+
+induction-triggers.dfy(37,39): Info: {:induction n}
+   |
+37 | lemma {:induction} {:inductionTrigger} Legacy2(n: nat) ensures f(n + 0) {}
+   |                                        ^^^^^^^
+
+induction-triggers.dfy(20,2): Info: ensures f(ih_n)
+   |
+20 |   forall ih_n: nat | (n decreases to ih_n) {
+   |   ^^^^^^
+
+induction-triggers.dfy(14,58): Error: a postcondition could not be proved on this return path
+   |
+14 | lemma {:induction false} NoInduction(n: nat) ensures f(n) {}
+   |                                                           ^
+
+induction-triggers.dfy(14,53): Related location: this is the postcondition that could not be proved
+   |
+14 | lemma {:induction false} NoInduction(n: nat) ensures f(n) {}
+   |                                                      ^^^^
+
+induction-triggers.dfy(4,47): Related location: this proposition could not be proved
+  |
+4 | predicate f(n: nat) { if n == 0 then true else f(n-1) }
+  |                                                ^^^^^^
+
+induction-triggers.dfy(26,42): Error: a postcondition could not be proved on this return path
+   |
+26 | lemma NoTriggers(n: nat) ensures f(n + 0) {}
+   |                                           ^
+
+induction-triggers.dfy(26,33): Related location: this is the postcondition that could not be proved
+   |
+26 | lemma NoTriggers(n: nat) ensures f(n + 0) {}
+   |                                  ^^^^^^^^
+
+induction-triggers.dfy(4,47): Related location: this proposition could not be proved
+  |
+4 | predicate f(n: nat) { if n == 0 then true else f(n-1) }
+  |                                                ^^^^^^
+
+
+Dafny program verifier finished with 14 verified, 2 errors