diff options
Diffstat (limited to 'Test/test21/PolyList.bpl')
-rw-r--r-- | Test/test21/PolyList.bpl | 134 |
1 files changed, 67 insertions, 67 deletions
diff --git a/Test/test21/PolyList.bpl b/Test/test21/PolyList.bpl index 08fcd637..f7ff40d6 100644 --- a/Test/test21/PolyList.bpl +++ b/Test/test21/PolyList.bpl @@ -1,68 +1,68 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t"
-// RUN: %diff "%s.n.expect" "%t"
-// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t"
-// RUN: %diff "%s.p.expect" "%t"
-// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t"
-// RUN: %diff "%s.a.expect" "%t"
-
-
-
-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
-
+// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" + + + +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 |