obj UserDB =  UserRecord*;
obj UserRecord =  ssn:number and ... ;

op AddRecord(udb:UserDB, ur:UserRecord)->(udb':UserDB)
    precondition:
        (* There is no record in the input database with the same key as that
         * of the given input record, where the key is defined as the SSN
         * field of the record. *)
        not (exists (ur':UserRecord) (ur' in udb') and (ur.ssn = ur'.ssn));
    postcondition:
        (* The given record is in the output database *)
        ur in udb';
end;