diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-10-31 15:30:58 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-10-31 15:30:58 -0700 |
| commit | 7d5178d5e5f652f8c3e0948b60adccb47f06d335 (patch) | |
| tree | e56cecb799f8608395f86a342ede272cc9ad38dc /Test/datatypes | |
| parent | 7c799c6f3536e873327213d74d01e7f1235b3ca8 (diff) | |
File to experiment with type encoding for .NET.
Diffstat (limited to 'Test/datatypes')
| -rw-r--r-- | Test/datatypes/t2.bpl | 42 |
1 files changed, 30 insertions, 12 deletions
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl index 26ffd337..2bca4e83 100644 --- a/Test/datatypes/t2.bpl +++ b/Test/datatypes/t2.bpl @@ -1,36 +1,54 @@ type {:datatype} DotNetType;
+/*\
+ * 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 NominalType2 : System.Object { ... }
-function {:constructor} NominalType2() : DotNetType;
-axiom $Subtype(NominalType2(), System.Object());
+// 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()));
-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));
+// 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)
{
assert System.Object() != GenericType1(t);
- assert System.Object() != NominalType2();
+ assert System.Object() != B();
}
procedure bar(t : DotNetType, u : DotNetType)
requires t != u;
{
assert System.Object() != GenericType1(t);
- assert System.Object() != NominalType2();
+ assert System.Object() != B();
assert GenericType1(t) != GenericType1(u);
}
|