diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-10-30 11:44:48 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-10-30 11:44:48 -0700 |
| commit | 2901a36002b6b7ed31e925525e3eab1f63aaa848 (patch) | |
| tree | 841f2dff7145225989be08eaa696f27d6e5f9c3b /Test/datatypes/t2.bpl | |
| parent | 937f5d2cbbf55ae5be84441b882b7a9d318d7dc8 (diff) | |
Removed prover option from runtest.bat because smtlib is now the default
in Boogie.
Added a test file for our encoding of .NET types in Boogie.
Diffstat (limited to 'Test/datatypes/t2.bpl')
| -rw-r--r-- | Test/datatypes/t2.bpl | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl new file mode 100644 index 00000000..26ffd337 --- /dev/null +++ b/Test/datatypes/t2.bpl @@ -0,0 +1,36 @@ +
+type {:datatype} DotNetType;
+
+// class System.Object { ... }
+function {:constructor} System.Object() : DotNetType;
+
+// class NominalType2 : System.Object { ... }
+function {:constructor} NominalType2() : DotNetType;
+axiom $Subtype(NominalType2(), 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));
+
+procedure foo(t : DotNetType)
+{
+ assert System.Object() != GenericType1(t);
+ assert System.Object() != NominalType2();
+}
+
+procedure bar(t : DotNetType, u : DotNetType)
+ requires t != u;
+{
+ assert System.Object() != GenericType1(t);
+ assert System.Object() != NominalType2();
+ assert GenericType1(t) != GenericType1(u);
+}
+
|