Automatic generation produced by ISE Eiffel
indexing
description: "Deferred Class that is a template for all User Data Access Classes"
author: "Marco Piccioni, Peizhu Li"
date: "$Date$"
revision: "$0.6$"
deferred class interface
USER_MANAGER
feature -- Attributes
user_list: HASH_TABLE [USER, STRING_8]
encryptor: ENCRYPTOR
-- encrypt user login name and password, void to skip encryption
feature --Basic Operations
add_user (a_user: USER)
--adds a user to the userlist
require
a_user_valid: a_user /= Void
user_not_exists: not username_defined (a_user.username)
ensure
one_user_added: user_list.count = old user_list.count + 1
update_user (a_user: USER)
--update a existing user
require
a_user_valid: a_user /= Void
user_exists: username_defined (a_user.username)
ensure
same_user_number: user_list.count = old user_list.count
delete_user_by_name (username: STRING_8)
--
require
username_exists: username /= Void and then not username.is_empty and then user_list.has (username)
ensure
one_user_removed: user_list.count = old user_list.count - 1
get_user_by_name (username: STRING_8): USER
-- return the USER object identified by username
require
username_exists: username /= Void and then not username.is_empty and then user_list.has (username)
ensure
user_found: Result /= Void
username_defined (username: STRING_8): BOOLEAN
--adds a user to the userlist
require
username_valid: username /= Void and then not username.is_empty
is_user_authentication_valid (username, pass: STRING_8): BOOLEAN
-- check user authentication
require
name_pass_not_empty: username /= Void and then not username.is_empty and then pass /= Void and then not pass.is_empty
set_encryptor (cryptor: ENCRYPTOR)
-- retrieve the saved session object with given session_id
user_count: INTEGER_32
--
persist_data
invariant
invariant_clause: True
end -- class USER_MANAGER
-- Generated by ISE Eiffel --
For more details: www.eiffel.com