class EDC_SQLITE_CONNECTION
require
- is_connected
- not name.is_empty
ensure
- Result.is_active
- Result.name.is_equal(name)
require
- is_connected
- a_savepoint.is_active
ensure
- not a_savepoint.is_active
set_auto_commit (a_auto_commit:
BOOLEAN)
effective procedure
require
ensure
- auto_commit = a_auto_commit
require
- a_table.connection = Void
-
new_table: not has_table_name(a_table.name)
-
has_columns: a_table.count_column > 0
ensure
- a_table.connection = Current
require
-
known_table: a_table.connection = Current
require
- not a_table_name.is_empty
require
- has_table_name(a_table_name)
ensure
- Result.for_all(has_table_name())
set_fetch_direction (a_fetch_direction:
INTEGER_32)
effective procedure
require
- a_fetch_direction = Fetch_forward or else a_fetch_direction = Fetch_backward
ensure
- fetch_direction = a_fetch_direction
ensure
- Result = Fetch_forward or else Result = Fetch_backward
require
ensure
-
commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)