diff options
| author |  Jason Koenig <unknown> | 2012-06-13 11:54:11 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-06-13 11:54:11 -0700 |
| commit | 7cabbe6e10f11b90df4e4b5f5a3bb1c2253b87c5 (patch) | |
| tree | 3600184e04e2deac3734da843283940361571fc6 /Test/dafny0/LiberalEquality.dfy | |
| parent | f2eb93519ffd02b775d427d2909cebd0690dc090 (diff) | |
Dafny: liberalized equality to work when the types could possibly be the same
(i.e. a != b is allowed when a: array<int> and b: array<T>)
Diffstat (limited to 'Test/dafny0/LiberalEquality.dfy')
| -rw-r--r-- | Test/dafny0/LiberalEquality.dfy | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy new file mode 100644 index 00000000..3dc52c80 --- /dev/null +++ b/Test/dafny0/LiberalEquality.dfy @@ -0,0 +1,55 @@ +
+class Array<T>
+{
+ var Length: nat;
+}
+
+class Test<T> {
+ var a: Array<int>;
+ var b: Array<T>;
+ predicate valid()
+ reads this, a, b;
+ {
+ a != null && b != null && a != b && a.Length == b.Length
+ }
+}
+
+method m1<T, U>(t: T, u: U)
+ requires t != u;
+{
+
+}
+
+method m2<T>(t: array<T>, a: array<int>)
+ requires t != null && a != null && t != a && t.Length == a.Length;
+{
+
+}
+
+
+class Weird<T, U, V>
+{
+
+}
+
+
+method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)
+ requires a == b; // Bad: second parameter can't be both bool and int.
+{
+
+}
+
+
+method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)
+ requires a == b;
+{
+
+}
+
+
+// Just to make sure nothing went wrong.
+method m5(a: array<int>, b: array<bool>)
+ requires a == b; // Bad: never equal
+{
+
+}
|