1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
type ref; type Wicket; const w: Wicket; var favorite: Wicket; function age(Wicket) returns (int); axiom age(w)==7; procedure NewFavorite(p: Wicket); modifies favorite ; ensures favorite==p; implementation NewFavorite(l: Wicket) { favorite:=l; }