+
Point of view
All features
class BINARY_FILE_WRITE
features
- buffer: NATIVE_ARRAY[CHARACTER]
- buffer_position: INTEGER_32
- capacity: INTEGER_32
- output_stream: POINTER
- make
- dispose
- write_buffer
- put_16_ne (buf: NATIVE_ARRAY[CHARACTER], i: INTEGER_16, ch_pos: INTEGER_32)
- put_16_le (buf: NATIVE_ARRAY[CHARACTER], i: INTEGER_16, ch_pos: INTEGER_32)
- put_16_be (buf: NATIVE_ARRAY[CHARACTER], i: INTEGER_16, ch_pos: INTEGER_32)
- put_32_ne (buf: NATIVE_ARRAY[CHARACTER], i: INTEGER_32, ch_pos: INTEGER_32)
- put_32_le (buf: NATIVE_ARRAY[CHARACTER], i: INTEGER_32, ch_pos: INTEGER_32)
- put_32_be (buf: NATIVE_ARRAY[CHARACTER], i: INTEGER_32, ch_pos: INTEGER_32)
- binary_file_write_open (path_pointer: POINTER): POINTER
- binary_file_write_append (path_pointer: POINTER): POINTER
- putc (byte: CHARACTER, stream: POINTER)
- fwrite (buf: NATIVE_ARRAY[CHARACTER], size: INTEGER_32, stream: POINTER)
- io_flush (stream_pointer: POINTER)
- fclose (stream_pointer: POINTER)
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