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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
trait TT
{
function method Plus(x:int, y:int) : int
requires x > y
{
x + y
}
function method Times(x:int, y:int) : int
requires x > y
static function method StaticMinus(x:int, y:int) : int
requires x > y
{
x - y
}
method Double(x: int)
{
print "d=", x+x, "\n";
}
method AddFive(x: int)
static method StaticTriple(x: int)
{
print "t=", 3*x, "\n";
}
}
class CC extends TT
{
function method Times(x:int, y:int) : int
requires x>y
{
x * y
}
method AddFive(x: int)
{
print "a5=", x+5, "\n";
}
}
method Client(t: TT)
requires t != null
{
var x := t.Plus(10, 2);
print "x=", x, "\n";
t.Double(400);
t.AddFive(402);
t.StaticTriple(404);
}
method Main()
{
var c := new CC;
var y := c.Plus(100, 20);
print "y=", y, "\n";
Client(c);
var z := TT.StaticMinus(50, 20);
print "z=", z, "\n";
var z' := CC.StaticMinus(50, 20);
print "z'=", z', "\n";
var w := c.StaticMinus(50, 20);
print "w=", w, "\n";
c.Double(500);
c.AddFive(502);
c.StaticTriple(504);
TT.StaticTriple(504);
CC.StaticTriple(505);
var seven := OtherModule.Y.F(15);
assert seven == 7;
var b := OtherModule.Y.P(real(seven));
print "From OtherModule.Y: ", seven, " and ", b, "\n";
seven := OtherModule.X.F(15);
assert seven == 7;
b := OtherModule.X.P(real(seven));
print "From OtherModule.X: ", seven, " and ", b, "\n";
TestFields.Test();
}
module OtherModule {
trait Y {
static function method F(x: int): int
{ x / 2 }
static method P(t: real) returns (f: bool)
{
print "This is OtherModule.P(", t, ")\n";
f := t < 10.0;
}
}
class X extends Y {
}
}
module TestFields {
trait J {
var f: int
}
class C extends J {
}
method Test() {
var c := new C;
var j: J := c;
c.f := 15;
assert j.f == 15;
print "c.f= ", c.f, " j.f= ", j.f, "\n";
j.f := 18;
assert c.f == 18;
print "c.f= ", c.f, " j.f= ", j.f, "\n";
}
}
|
