blob: 55897a1d10213a565499b01f21e6e3a711c40930 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
// types
type Wicket;
var favorite: Wicket;
function age(w:Wicket) returns (int);
axiom (forall v:Wicket :: age(v)==7);
axiom (exists v:Wicket :: age(v)<8);
// procedure
procedure SetToSeven(p: Wicket);
modifies favorite
;
ensures favorite==p;
implementation SetToSeven(l: Wicket) {
favorite:=favorite;
}
|
