1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
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; // Cannot compare type parameters (can only compare reference types that could be the same)
{
}
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
{
}
|
