obj Rolodex =  state:SystemState and cards:CardList; (* Same as above *)
obj SystemState =  (* previous components and *) prev:CardList;
obj Card =  (* as usual *);

op Add(r:Rolodex, c:Card)->(r':Rolodex)
    post:
        (* The following is the original postcond, with substitution
         * of r.cards for r and r'.cards for r' *)
        forall (c':Card)
            (c' in r'.cards) iff ((c' in r.cards) or (c' = c))

            and

        (* Save the cards of the input Rolodex as the previous card list. *)
        (r'.state.prev = r.cards);

end Add;

op Undo(r: Rolodex)->(r':Rolodex)
    post:
        (* If the input Rolodex has a previous card list,
         * then the cards of the output Rolodex are that list
         * and the previous of the output is nil (so only one
         * level of undo is possible).
         * Otherwise, the output Rolodex is the same as the
         * input Rolodex. *)
        if (r.state.prev != nil)
        then (r'.cards = r.state.prev) and (r'.state.prev = nil)
        else r' = r;
end;