indexing
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
product: eiffelstore
database: all_bases
class interface
DB_REPOSITORY
create
make (name: STRING)
name
require
name_exists: name /= void
ensure
repository_name.is_equal (name)
feature
make (name: STRING)
name
require
name_exists: name /= void
ensure
repository_name.is_equal (name)
feature
column_i_th (i: INTEGER): COLUMNS [DATABASE]
require
indice_valid: i >= 1 and i <= column_number
ensure
Result /= void
column_number: INTEGER
ensure
Result >= 0
feature
conforms (object: ANY): BOOLEAN
object
repository_name
require
parameter_not_void: object /= void
is_loaded: loaded
is_ok: is_ok
exists: BOOLEAN
repository_name
require
is_ok: is_ok
rep_loaded: loaded
loaded: BOOLEAN
repository_name: STRING
feature
is_connected: BOOLEAN
DB_STATUS_USE
is_ok: BOOLEAN
DB_STATUS_USE
feature
allocate (object: ANY)
object
require
connected: is_connected
obj_exists: object /= void
is_ok: is_ok
change_name (new_name: STRING)
new_name
require
is_ok: is_ok
name_exists: new_name /= void
ensure
ensure_name (new_name)
generate_class (f: FILE)
require
is_ok: is_ok
rep_loaded: loaded
file_exists: f /= void and then f.exists
load
repository_name
require
repository_name: repository_name /= void
connected: is_connected
ensure
loaded
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- DB_REPOSITORY