+
Point of view
All features
class TEXT_FILE_WRITE
- is_connected implies path /= Void
Features
{}
{}
{}
{}
{}
{}
{}
{}
{}
require
- not is_connected
-
not_malformed_path: not new_path.is_empty
ensure
require
- is_connected
- can_disconnect
- is_connected
- can_disconnect
- is_connected
- can_disconnect
ensure
require
-
locked: tagged_out_locked
-
locked: tagged_out_locked
-
locked: tagged_out_locked
-
locked: tagged_out_locked
ensure
-
still_locked: tagged_out_locked
-
not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
-
append_only: old tagged_out_memory.twin.is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))
require
- is_connected
- can_put_character(c)
require
- is_connected
- filtered_has_descriptor
- is_connected
- filtered_has_descriptor
- is_connected
- filtered_has_descriptor
is True
constant attribute
require
- is_connected
- filtered_has_stream_pointer
- is_connected
- filtered_has_stream_pointer
- is_connected
- filtered_has_stream_pointer
filtered_has_stream_pointer:
BOOLEAN
is True
constant attribute
ensure
-
definition: Result = path /= Void
ensure
- path.same_as(new_path.out)
frozen
effective function
ensure
-
not_void: Result /= Void
-
always_the_same: Result = url
require
- is_connected
- not is_filtered and then can_put_character(c)
ensure
-
yes_indeed_it_is_the_same_object: Result.to_pointer = to_pointer
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
frozen
effective procedure
append_file (file_name:
STRING)
effective procedure