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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module M0 {
class MyClass<T(==),U(==)> {
var s: map<T,set<U>>;
static function F<W>(w: W, w': W, t: T, u: U): int
{
if w == w' then 5 else 7
}
function G<Y>(y: Y): Y { y }
static function H<Y>(y: Y): (T, U, Y)
ghost method M() {
var f0 := F<int>;
var f1 := MyClass<int,bool>.F<real>;
var g0 := G;
var x := g0(500);
var g1 := G<real>;
var mc: MyClass<int,bool>, tt, uu, yy;
if mc != null {
var h0 := mc.H(5.0);
tt, uu, yy := h0.0, h0.1, h0.2;
if (tt, uu, yy) == MyClass.H(4.0) {
}
var h1 := MyClass.H(4.0); // error: types to MyClass underspecified
var h2 := MyClass<bool, int>.H(4.0);
var pt: T, pu: U;
var h3 := MyClass<T,U>.H(3.2);
h3 := MyClass.H(3.2);
pt := h3.0;
pu := h3.1;
var r := h3.2 + 0.3;
}
}
}
}
module M1 {
class C0 {
function method F(x: bool, y: bool): () { () }
method M0(a: int, b: int, c: int, d: int) {
var u := F( a < b , (c > (d)) );
var v := F( a < b , c > d );
}
method M1(a: int, b: int, c: int, d: int) {
var u := F( a < b , c > (d) ); // error: undefined types b,c; undefined function a; wrong # args to F
}
}
class C1 {
function method F(x: int): () { () }
function method a<T,U>(x: int): int { x }
method M<b, c>(d: int) {
var u;
u := F( a < b , c > (d) );
}
method P<g,h,m,n>() {
assert a<g,h> == a<m,n>;
}
}
}
module M2 {
class ClassA {
function F<A>(a: A): int
lemma Lem<Y>() returns (y: Y)
lemma M<X>(x: X)
{
var k := Lem<int>();
}
}
class ClassB {
lemma LemmaX<A>(y: A)
lemma LemmaY<A>(x: int)
{
LemmaX<A>(x); // error: The given type instantiation A does not agree with the type of parameter x
}
lemma LemmaR<T>(x: int)
lemma LemmaS<A>()
{
LemmaR<A>(5);
}
function FuncX<A>(y: A): real
function FuncY<A>(x: int): real
{
FuncX<A>(x) // error: The given type instantiation A does not agree with the type of parameter x
}
function FuncR<T>(x: int): real
function FuncS<A>(): real
{
FuncR<A>(5)
}
}
}
|
