package admin;

import java.util.Collection;
import java.lang.Integer;

/****
 *
 * Package admin defines the objects and operations related to maintaining the
 * user, group, location, and global options databases of the Calendar Tool.
 *
 */

abstract class UserDB {
    Collection <UserRecord> udb;

    /**
     * Add the given UserRecord ur to this.udb.  The UserId of the given user
     * record must not be the same as a user record already in the udb.  The
     * UserId component is required and must be eight characters or less.  The
     * email address is required.  The phone number is optional; if given, the
     * area code and number must be 3 and 7 digits respectively.
     */
    /*@
      requires
        //
        // There is no user record in the input UserDB with the same id as the
        // record to be added.
        //
        (! (\exists UserRecord ur_other ;
                udb.contains(ur_other) ;
                    ur_other.id == ur.id))

            &&

        //
        // The id of the given user record is not empty and 8 characters or
        // less.
        //
        (ur.id != null) && (ur.id.length() <= 8)

            &&

        //
        // The email address is not empty.
        //
        (ur.email != null)

            &&

        //
        // If the phone area code and number are present, they must be 3 digits
        // and 7 digits respectively.
        //
        ((ur.phone.area != 0)
            ? Integer.toString(ur.phone.area).length() == 3 : true) &&
        ((ur.phone.number != 0)
            ? Integer.toString(ur.phone.number).length() == 7 : true);

      ensures
        //
        // A user record is in the output db if and only if it is the new
        // record to be added or it is in the input db.
        //
        (\forall UserRecord ur_other ;
 	    udb.contains(ur_other) <==>
                (ur_other.equals(ur) || \old(udb).contains(ur_other)));

      @*/ 
    abstract void add(UserRecord ur);
}

abstract class UserRecord {
    String id;
    String email;
    PhoneNumber phone;
}

abstract class PhoneNumber {
    int area;
    int number;
}