blob: cf76e8604a3a1fee442d7d2beb1314476b1bcd50 (
plain)
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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
module m1
{
trait I1
{
function M1(x:int,y:int) :int
{
x*y
}
}
trait I2 //all is fine in this trait
{
var x: int;
function method Twice(): int
reads this;
{
x + x
}
function method F(z: int): int
reads this;
method Compute(s: bool) returns (t: int, u: int)
modifies this;
{
if s {
t, u := F(F(15)), Twice();
} else {
t := Twice();
x := F(45);
u := Twice();
var p := Customizable(u);
return t+p, u;
}
}
method Customizable(w: int) returns (p: int)
modifies this;
static method StaticM(a: int) returns (b: int)
{
b := a;
}
static method SS(a: int) returns (b:int)
{
b:=a*2;
}
}
method I2Client(j: I2) returns (p: int) //all is fine in this client method
requires j != null;
modifies j;
{
j.x := 100;
var h := j.Twice() + j.F(j.Twice());
var a, b := j.Compute(h < 33);
var c, d := j.Compute(33 <= h);
p := j.Customizable(a + b + c + d);
p := I2.StaticM(p);
}
class I0Child extends I2 //errors, body-less methods/functions in the parent have not implemented here
{
function method F(z: int): int
reads this;
{
z
}
var x: int; //error, x has been declared in the parent trait
}
class I0Child2 extends I2
{
method Customizable(w: int) returns (p: int)
modifies this;
{
w:=w+1;
}
var c1: I0Child;
}
class IXChild extends IX //error, IX trait is undefined
{
}
}
|
