+
Point of view
INTERNALS_HANDLER
class BINARY_FILE_WRITE
require
- not is_connected
-
not_malformed_path: not new_path.is_empty
ensure
- is_connected implies path.same_as(new_path)
connect_for_appending_to (new_path:
STRING)
effective procedure
ensure
-
definition: Result = path /= Void