diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-29 14:43:03 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-29 14:43:03 -0800 |
| commit | 08e9539279d31cfb650e0e55984216f5c8ffcd25 (patch) | |
| tree | 66f9cb5a66bdb193a535dc9003dba0c2546a6441 /Test/datatypes/t2.bpl | |
| parent | cc80320df0b652f25ffbd68a004b56c2ef34d981 (diff) | |
fixed problems with datatypes
removed stale contracts in stratified inlining
added test to datatypes
Diffstat (limited to 'Test/datatypes/t2.bpl')
| -rw-r--r-- | Test/datatypes/t2.bpl | 74 |
1 files changed, 18 insertions, 56 deletions
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl index f794b227..d4d2bf3f 100644 --- a/Test/datatypes/t2.bpl +++ b/Test/datatypes/t2.bpl @@ -1,62 +1,24 @@ +type TT;
+type {:datatype} Tree;
+function {:constructor} leaf`0() : Tree;
+function {:constructor} node`2(value:TT, children:TreeList) : Tree;
-type {:datatype} DotNetType;
+type {:datatype} TreeList;
+function {:constructor} cons`2(car:Tree, cdr:TreeList) : TreeList;
+function {:constructor} nil`0() : TreeList;
-/*\
- * Subtype Axioms
-\*/
-function $Subtype(DotNetType, DotNetType) : bool;
-// reflexive
-axiom (forall t: DotNetType :: $Subtype(t, t));
-// anti-symmetric
-axiom (forall t0: DotNetType, t1: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t0) } $Subtype(t0, t1) && $Subtype(t1, t0) ==> t0 == t1);
-// transitive
-axiom (forall t0: DotNetType, t1: DotNetType, t2: DotNetType :: { $Subtype(t0, t1), $Subtype(t1, t2) } $Subtype(t0, t1) && $Subtype(t1, t2) ==> $Subtype(t0, t2));
-
-/*\
- * Type Declarations
-\*/
-// class System.Object { ... }
-function {:constructor} System.Object() : DotNetType;
-
-// class B : System.Object { ... }
-function {:constructor} B() : DotNetType;
-axiom $Subtype(B(), System.Object());
-
-// class GenericType1<T> : System.Object { ... }
-function {:constructor} GenericType1(T:DotNetType) : DotNetType;
-axiom (forall t : DotNetType :: $Subtype(GenericType1(t), System.Object()));
-
-// class C : GenericType1<object>
-function {:constructor} C() : DotNetType;
-axiom $Subtype(C(), GenericType1(System.Object()));
-
-// class D<U> : GenericType1<U>
-function {:constructor} D(U:DotNetType) : DotNetType;
-axiom (forall u : DotNetType :: $Subtype(D(u), GenericType1(u)));
-
-// class GenericType2<T,U> : System.Object { ... }
-function {:constructor} GenericType2(T:DotNetType, U:DotNetType) : DotNetType;
-axiom (forall t : DotNetType, u : DotNetType :: $Subtype(GenericType2(t,u), System.Object()));
-
-
-procedure foo(t : DotNetType)
+procedure foo()
{
- assert System.Object() != GenericType1(t);
- assert System.Object() != B();
-}
+ var a: Tree;
+ var b: TreeList;
+ var x: TT;
-procedure bar(t : DotNetType, u : DotNetType)
- requires t != u;
-{
- assert System.Object() != GenericType1(t);
- assert System.Object() != B();
- assert GenericType1(t) != GenericType1(u);
-}
+ assert value#node`2(node`2(x, nil`0())) == x;
+ assert children#node`2(node`2(x, nil`0())) == nil`0();
+
+ assert (cons`2(leaf`0(), nil`0()) != nil`0());
-function IntToType(x : int) : DotNetType;
-procedure baz(i : int)
-{
- var t : DotNetType;
- t := IntToType(i);
- assert T#GenericType1(t) == System.Object();
+ assert is#nil`0(nil`0());
+
+ assert is#node`2(leaf`0());
}
\ No newline at end of file |