1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
// types type Wicket; // consts var favorite: Wicket; // axioms const b: bool; axiom b==true; // procedure procedure SetToSeven(p: Wicket); modifies favorite ; ensures favorite==p; implementation SetToSeven(l: Wicket) { favorite:=l; }