blob: 2c18907f0536da0ec9f55087d6a179bafb88fcde (
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
|
class A {
method m(i: int) returns (x: int)
ensures x == i;
{
var j := 0;
var v [v == i + j];
x := v;
}
method n() {
var x := 0;
var y := 1;
var z := 2;
}
}
class B refines A {
transforms m(i: int) returns (x: int, y: int)
ensures y == 0;
{
var t := 0;
_
replaces v by {
var v := i + j;
call t, j := m(0);
y := j;
}
_
}
transforms n() {
replaces * by {
var x := 0;
var y := x + 1;
var z := 2*y;
}
}
}
|