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/PolyList.bpl | |
Initial set of files.
Diffstat (limited to 'Test/test21/PolyList.bpl')
| -rw-r--r-- | Test/test21/PolyList.bpl | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/Test/test21/PolyList.bpl b/Test/test21/PolyList.bpl new file mode 100644 index 00000000..49d515f9 --- /dev/null +++ b/Test/test21/PolyList.bpl @@ -0,0 +1,62 @@ +
+
+
+type List a;
+
+function Cons<a>(x:a, y:List a) returns (List a);
+
+// we need some argument ... ugly
+function Nil<a>(a) returns (List a);
+
+function Car<a>(List a) returns (a);
+function Cdr<a>(List a) returns (List a);
+
+axiom (forall<a> x:a, y:List a :: Car(Cons(x, y)) == x);
+axiom (forall<a> x:a, y:List a :: Cdr(Cons(x, y)) == y);
+
+function Len<a>(List a) returns (int);
+
+axiom (forall <a> x:a :: Len(Nil(x)) == 0);
+axiom (forall <a> x:a, y:List a :: Len(Cons(x, y)) == 1 + Len(y));
+
+
+
+procedure P<a>(param : a) returns () {
+ var x:a, NIL : List a, l : List a;
+
+ NIL := Nil(x);
+
+ assert Len(NIL) == 0;
+ assert Len(Cons(x,Cons(x,NIL))) == 2;
+
+ l := Cons(x,Cons(x,NIL));
+ assert Len(l) == 2;
+
+ l := Cons(x, l);
+ assert Len(l) == 3 && Car(l) == x && Len(Cdr(l)) < Len(l);
+ assert (forall m : List a, y : a :: Len(Cons(y, m)) > Len(m));
+
+ l := Cdr(l);
+ assert Len(l) == 2 && Car(l) == x;
+
+ assert Len(Cons(x,Cons(x,Cons(x,NIL)))) == 2; // should not be provable
+
+}
+
+procedure Q() returns () {
+ var NIL : List int, l : List int;
+
+ NIL := Nil(0);
+
+ assert Len(NIL) == 0;
+ assert Len(Cons(1,Cons(2,NIL))) == 2;
+
+ l := NIL;
+ l := Cons(42, l);
+ l := Cons(Car(l) + 17, Cdr(l));
+
+ assert Len(l) == 1 && Car(l) == 59;
+
+ assert Len(Cons(1,Cons(2,Cons(3,NIL)))) == 2; // should not be provable
+
+}
\ No newline at end of file |