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/test21/DisjointDomains2.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test21/DisjointDomains2.bpl')
| -rw-r--r-- | Test/test21/DisjointDomains2.bpl | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/Test/test21/DisjointDomains2.bpl b/Test/test21/DisjointDomains2.bpl new file mode 100644 index 00000000..3cac88ca --- /dev/null +++ b/Test/test21/DisjointDomains2.bpl @@ -0,0 +1,64 @@ +type C _;
+
+function f<a>(C a) returns (int);
+
+axiom (forall<a> x : C a :: f(x) == 42);
+
+procedure P(a : C int) returns () {
+
+ start:
+ assert f(a) == 42;
+ assert f(a) == 43; // should not be provable
+}
+
+procedure Q<a>(c : C a) returns () {
+
+ start:
+ assert f(c) == 42;
+ assert f(c) == 43; // should not be provable
+}
+
+function g<a,b>(a, b) returns (int);
+
+
+axiom (forall x : int, y : bool :: g(x,y) == 13);
+axiom (forall<a> x : int, y : C a :: g(x,y) == 42);
+axiom (forall<a,z> x : C z, y : C a :: g(x,y) == 43);
+
+procedure R() returns () {
+
+ start:
+ assert g(7, true) == 13;
+ assert g(7, false) == 15; // should not be provable
+}
+
+procedure S<b>(y : C b) returns () {
+
+ start:
+ assert g(3, y) == f(y);
+ assert g(y, false) == 15; // should not be provable
+}
+
+procedure T<a,b>(y : C b, param : a) returns () {
+ var x : C a; var z : C b;
+
+ start:
+ assert g(y, x) == g(x, y);
+ assert g(y, x) == 43;
+ assert g(f(x), y) == 42;
+ assert g(y, z) == 15; // should not be provable
+}
+
+
+type D _ _;
+
+procedure U() returns () {
+ var u : D int bool, v : D bool int;
+
+ start:
+ assume (forall<a,b> x:D a b, y:b :: g(x, y) == -3);
+
+ assert g(v, 32) == -3;
+ assert g(v, 716371398712982312321) == -3;
+ assert g(u, 1) == -3; // should not be provable
+}
|