blob: 3bd6ff634a55db6ad4db0714b15e5c1de8919ece (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
type ref;
// 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;
}
|
