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
type ref; // types type Wicket; var favorite: Wicket; var v: Wicket; function age(w:Wicket) returns (int); axiom (exists v:Wicket :: age(v)<8 && (forall v:Wicket :: age(v)==7) ); // procedure procedure SetToSeven(p: Wicket); modifies favorite ; ensures favorite==p; implementation SetToSeven(l: Wicket) { favorite:=favorite; }