val ur:UserRecord = {"Corwin", "1", "pccorwin@calpoly.edu", nil};
val udb:UserDB = [];

operation AddUser
    inputs: udb:UserDB, ur:UserRecord;
    outputs: udb':UserDB;

    precondition:
        (*
         * There is no user record in the input UserDB with the same id as the
         * record to be added.
         *)
        (not (exists (ur' in udb) ur'.id = ur.id))

            and

        (*
         * The id of the given user record is not empty and 8 characters or
         * less.
         *)
        (ur.id != nil) and (#(ur.id) <= 8)

            and

        (*
         * The email address is not empty.
         *)
        (ur.email != nil)

            and

        (*
         * If the phone area code and number are present, they must be 3 digits
         * and 7 digits respectively.
         *)
        (if (ur.phone.area != nil) then (#(ur.phone.area) = 3)) and
        (if (ur.phone.num != nil) then (#(ur.phone.num) = 7));


    postcondition: (* Same as above *);

end AddUser;
> AddUser(udb,ur)?->(udb);
> (not (exists (ur' in udb) ur'.id = ur.id));
> (ur.id != nil) and (#(ur.id) <= 8);
> (ur.email != nil);
> (if (ur.phone.area != nil) then (#(ur.phone.area) = 3));
> (if (ur.phone.num != nil) then (#(ur.phone.num) = 7));
> (not (exists (ur' in udb) ur'.id = ur.id)) and
  (ur.id != nil) and (#(ur.id) <= 8) and
  (ur.email != nil) and
  (if (ur.phone.area != nil) then (#(ur.phone.area) = 3)) and
  (if (ur.phone.num != nil) then (#(ur.phone.num) = 7));
>         (*
         * There is no user record in the input UserDB with the same id as the
         * record to be added.
         *)
        (not (exists (ur' in udb) ur'.id = ur.id))

            and

        (*
         * The id of the given user record is not empty and 8 characters or
         * less.
         *)
        (ur.id != nil) and (#(ur.id) <= 8)

            and

        (*
         * The email address is not empty.
         *)
        (ur.email != nil)

            and

        (*
         * If the phone area code and number are present, they must be 3 digits
         * and 7 digits respectively.
         *)
        (if (ur.phone.area != nil) then (#(ur.phone.area) = 3)) and
        (if (ur.phone.num != nil) then (#(ur.phone.num) = 7));