home
wiki
classes/clusters list
class information
+
Point of view
All features
ANY
INTERNALS_HANDLER
All features
class STREAM_SPLICE
Summary
top
Direct parents
insert list:
ANY
Class invariant
top
is_connected
implies
instream
.is_connected
is_connected
implies
outstream
.is_connected
Overview
top
creation features
connect_to
(a_instream:
INPUT_STREAM
, a_outstream:
OUTPUT_STREAM
)
Connect streams
make
Create a non-connected splice
features
connect_to
(a_instream:
INPUT_STREAM
, a_outstream:
OUTPUT_STREAM
)
Connect streams
disconnect
Disconnect streams
is_connected
:
BOOLEAN
Are streams connected?
splice
Move data from instream to outstream while there is anything to move, using an internal stack.
splice_in_stack
(a_stack:
LOOP_STACK
)
Puts a job in
a_stack
that moves data from instream to outstream.
make
Create a non-connected splice
splice_stack
:
LOOP_STACK
A stack for splice jobs.
job
:
SPLICE_JOB
The job that will be placed on the stack
instream
:
STREAM
outstream
:
STREAM
connect_to
(a_instream:
INPUT_STREAM
, a_outstream:
OUTPUT_STREAM
)
effective procedure
top
Connect streams
require
not
is_connected
a_instream.is_connected
a_outstream.is_connected
ensure
is_connected
disconnect
effective procedure
top
Disconnect streams
require
is_connected
ensure
not
is_connected
old
instream
.is_connected = old
instream
.is_connected
old
outstream
.is_connected = old
outstream
.is_connected
is_connected
:
BOOLEAN
effective function
top
Are streams connected?
ensure
Result implies
instream
/= Void
Result implies
outstream
/= Void
splice
effective procedure
top
Move data from instream to outstream while there is anything to move, using an internal stack.
See also
splice_in_stack
.
require
is_connected
splice_in_stack
(a_stack:
LOOP_STACK
)
effective procedure
top
Puts a job in
a_stack
that moves data from instream to outstream.
No provision is made to start the stack.
See also
splice
.
require
is_connected
make
effective procedure
top
Create a non-connected splice
splice_stack
:
LOOP_STACK
once function
top
A stack for splice jobs.
See
splice
.
job
:
SPLICE_JOB
writable attribute
top
The job that will be placed on the stack
instream
:
STREAM
effective function
top
outstream
:
STREAM
effective function
top