+
Point of view
All features
class STREAM_PROTOCOL
Summary
A protocol used for internal purposes: implementation of STREAM.url
Direct parents
Inherit list: PROTOCOL
Class invariant
Overview
Creation features
{URL}
Features
{ANY}
{URL_VALIDITY}
{URL}
{}
{RECYCLING_POOL}
  • recycle
    Do whatever needs to be done to free resources or recycle other objects when recycling this one
{}
  • dispose
    Action to be executed just before garbage collection reclaims an object.
effective function
{ANY}
is_connected: BOOLEAN
effective function
{ANY}
error: STRING
effective function
{ANY}
valid_uri (a_uri: STRING): BOOLEAN
effective function
connect_to (url: URL, read: BOOLEAN, write: BOOLEAN)
effective procedure
{URL}
require(
  • True
) or else (
    • url.uri /= Void
    • not is_connected
    • read or write
)
disconnect
effective procedure
{URL}
require
  • is_connected
ensure
  • not is_connected
input: INPUT_STREAM
effective function
{URL}
require
  • is_connected
output: OUTPUT_STREAM
effective function
{URL}
require
  • is_connected
locator (a_uri: STRING): RESOURCE_LOCATOR
effective function
{URL}
PROTOCOL is a factory of RESOURCE_LOCATOR
require
  • valid_uri(a_uri)
ensure
  • Result.uri.is_equal(a_uri)
recycle_locator (a_locator: RESOURCE_LOCATOR)
effective procedure
{URL}
require
  • a_locator /= Void
make (a_stream: STREAM)
effective procedure
{}
require
  • a_stream /= Void
stream: STREAM
writable attribute
{}
instream: INPUT_STREAM
writable attribute
{}
outstream: OUTPUT_STREAM
writable attribute
{}
recycle
effective procedure
Do whatever needs to be done to free resources or recycle other objects when recycling this one
dispose
effective procedure
{}
Action to be executed just before garbage collection reclaims an object.