obj SystemState =  (* previous components and *)
        users:UserTable and addok:boolean;
obj UserTable =  UserInfo*;
obj UserInfo =  uid:UserId and level:Level;
obj UserId =  string;
obj Level =  priv:Privileged or nonpriv:Nonprivileged;
obj Privileged;
obj Nonprivileged;

op Login(uid:UserId,state:SystemState)->(r':Rolodex)
    post:
        (* Adds are OK in the output Rolodex if the given user
         * is privileged, otherwise adds are not OK. *)
        if FindUser(state.users,uid).level?.priv
        then r'.state.addok = true
        else r'.state.addok = false

            and

        (* The output Rolodex has no cards. *)
        (r'.cards = nil);

    description: (*
        The operational model here is that the login operation creates an
        initial empty Rolodex, with the appropriate value for the addok flag.
        This model affects the specification of the File Open operation, in
        that the Open will read Rolodex cards from a file, but maintain the
        Rolodex state established by Login. *);
end;

op FindUser(ut:UserTable,uid:UserId)->(uinfo:UserInfo)
    pre:
	exists (uinfo' in ut) uinfo'.uid = uid;
    post:
	(uinfo in ut) and (uinfo.uid = uid);
end;