blob: 36f952d1d3a6a09aca842201d73492a3abb663ce (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
// consts
const w: int;
// vars
var favorite: int;
// procedure
procedure SetToSeven(p: int);
modifies favorite
;
ensures favorite==p;
implementation SetToSeven(l: int) {
favorite:=w;
}
|