diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Test/test2/CallForall.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test2/CallForall.bpl')
| -rw-r--r-- | Test/test2/CallForall.bpl | 134 |
1 files changed, 134 insertions, 0 deletions
diff --git a/Test/test2/CallForall.bpl b/Test/test2/CallForall.bpl new file mode 100644 index 00000000..98a62103 --- /dev/null +++ b/Test/test2/CallForall.bpl @@ -0,0 +1,134 @@ +function G(int) returns (int);
+axiom (forall x: int :: { G(x) } 0 <= x ==> G(x) == x);
+
+function F(int) returns (int);
+axiom (forall x: int :: { F(G(x)) } 0 <= x ==> F(G(x)) == 5);
+
+procedure Lemma(y: int)
+ requires 0 <= y;
+ ensures F(y) == 5;
+{
+ // proof:
+ assert G(y) == y;
+}
+
+procedure Main0()
+{
+ assert F(2) == 5; // error: cannot prove this directly, because of the trigger
+}
+
+procedure Main1()
+{
+ call Lemma(2);
+ assert F(2) == 5;
+}
+
+procedure Main2()
+{
+ call Lemma(3);
+ assert F(2) == 5; // error: Lemma was instantiated the wrong way
+}
+
+procedure Main3()
+{
+ call forall Lemma(*);
+ assert F(2) == 5;
+}
+
+procedure Main4()
+{
+ call forall Lemma(*);
+ assert false; // error
+}
+
+procedure Main5(z: int)
+{
+ call forall Lemma(*);
+ assert F(z) == 5; // error: z might be negative
+}
+
+procedure Main6(z: int)
+ requires 0 <= z;
+{
+ call forall Lemma(*);
+ assert F(z) == 5;
+}
+
+// ------------ several parameters
+
+function K(int, int) returns (int);
+axiom (forall x: int, y: int :: { K(G(x), G(y)) } 0 <= x && 0 <= y ==> K(G(x), G(y)) == 25);
+
+procedure MultivarLemma(x: int, y: int)
+ requires 0 <= x;
+ requires 0 <= y;
+ ensures K(x,y) == 25;
+{
+ // proof:
+ assert G(x) == x;
+ assert G(y) == y;
+}
+
+procedure Multi0(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ assert K(x,y) == 25; // error
+}
+
+procedure Multi1(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ call MultivarLemma(x, y);
+ assert K(x,y) == 25;
+}
+
+procedure Multi2(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ call forall MultivarLemma(x, y);
+ assert K(x,y) == 25;
+}
+
+procedure Multi3(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ call forall MultivarLemma(*, y);
+ assert K(x,y) == 25;
+}
+
+procedure Multi4(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ call forall MultivarLemma(x, *);
+ assert K(x,y) == 25;
+}
+
+procedure Multi5(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ call forall MultivarLemma(2 + 100, *);
+ assert K(102, y) == 25;
+ assert false; // error
+}
+
+procedure Multi6(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ call forall MultivarLemma(*, y);
+ assert K(x+2,y+2) == 25; // error
+}
+
+procedure Multi7(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ call forall MultivarLemma(x, *);
+ assert K(x+2,y+2) == 25; // error
+}
+
+procedure Multi8(x: int, y: int)
+ requires 0 <= x && 0 <= y;
+{
+ call forall MultivarLemma(*, *);
+ assert K(x+2,y+2) == 25; // that's the ticket!
+}
+
|