Automatic generation produced by ISE Eiffel

ClassesClustersCluster hierarchyChartRelationsTextFlatContractsFlat contracts
indexing
    description: "Objects help retrieving/saving/deleting sessions"
    author: "Peizhu Li, <lip@student.ethz.ch>"
    date: "05.01.2008"
    revision: "$0.6$"

deferred class 
    SESSION_MANAGER

feature -- attributes	

    session_id_length: INTEGER_32
            -- number of digits/characters used for session id
    
feature {SESSION_MANAGER} -- attributes	

    random_number_generator: RANDOM
            -- generate new session id

    last_random: INTEGER_32
            -- last generated string, used as next seed
    
feature -- operations

    generate_session_id: STRING_8
            -- generate a new session id
        local
            int_formatter: FORMAT_INTEGER
        do
            make_random_number
            create int_formatter.make (last_random)
            int_formatter.set_width (session_id_length)
            int_formatter.set_fill ('0')
            int_formatter.zero_fill
            create Result.make_from_string (int_formatter.formatted (last_random).out)
            check
                session_id_width_ok: Result.count = session_id_length
            end
        end

    get_session (sid: STRING_8): SESSION
            -- retrieve the saved session object with given session_id
            -- otherwise return void
        require
            sid_session_valid: sid /= Void and then not sid.is_empty
        deferred
        end

    save_session (sid: STRING_8; session: SESSION)
            -- save given session information
        require
            sid_session_valid: sid /= Void and then not sid.is_empty and then session /= Void
        deferred
        end

    delete_session (sid: STRING_8)
            -- delete a session based on given id
        deferred
        end

    cleanup
            -- consolidate saved session information, clean-up expired/invalid sessions in storage (files/db)
        deferred
        end
    
feature {NONE} -- Implementation

    init_manager (expiration, sid_length: INTEGER_32)
            -- initialize random_number_generator and last_random
        local
            time: TIME
        do
            create time.make_now
            create random_number_generator.set_seed (time.milli_second)
            last_random := random_number_generator.next_random (time.milli_second)
            session_id_length := sid_length
        end

    make_random_number
            -- make a new random number and store it in 'last_random'
        do
            last_random := random_number_generator.next_random (last_random)
        end
    
invariant
    invariant_clause: True

end -- class SESSION_MANAGER
ClassesClustersCluster hierarchyChartRelationsTextFlatContractsFlat contracts

-- Generated by ISE Eiffel --

For more details: www.eiffel.com