operation InitiateAdd(r:Rolodex)->(cd:CardData)
    post:
        (* If the historical dialog option is on, then output the previously
         * entered card data, else output empty card data. *)
        if r.state.options.showprevdata
        then cd.c = r.state.lastadd
        else cd.c = nil;
end;

operation ConfirmAdd(r:Rolodex, cd:CardData)->(r':Rolodex)
    pre: (* Same precondition as original Add,  but replace all occurrences of
          * variable c with cd.c *);
    post: (* Same postcondition as original Add, with same replacements as in
           * precondition *);
end;

obj CardData =  c:Card and flag:boolean
    description: (* See discussion below *);
end;

object Rolodex =  state:SystemState and cards:Card*;
object SystemState =  lastadd:LastAddInput and LastDeleteInput
        and LastChangeInput and LastSearchInput and options:Options;
object LastAddInput =  Card;
object LastDeleteInput =  Name;
object LastChangeInput =  Name and Card;
object LastSearchInput =  SearchInfo;
object Options =  showprevdata:ShowPreviousData  and ... ;
object ShowPreviousData =  boolean;