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 ubd';
end;

op AddRecord2(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' in udb') (ur.ssn = ur'.ssn));
    postcondition:
        (* The given record is in the output database *)
        ur in ubd';
end;