Eiffeldoc: EIFFELTEST_COMMAND_PROVIDER

+

Point of view

All features

class EIFFELTEST_COMMAND_PROVIDER

Summary

Direct parents: Insert list: ANY

Class invariant

commands /= Void
disconnected_clients /= Void

Overview

Creation features

make

Features

add (a_path: STRING)
display (stream: OUTPUT_STREAM)
count: INTEGER_32
is_empty (client: EIFFELTEST_CLIENT_SOCKET): BOOLEAN
item (client: EIFFELTEST_CLIENT_SOCKET): FIXED_STRING
remove (client: EIFFELTEST_CLIENT_SOCKET)

{}

add (a_path: STRING)

effective procedure

require

a_path /= Void

ensure

count > 0

display (stream: OUTPUT_STREAM)

effective procedure

require

stream.is_connected

count: INTEGER_32

effective function

is_empty (client: EIFFELTEST_CLIENT_SOCKET): BOOLEAN

effective function

ensure

Result implies count = 0
count > 0 implies not Result

item (client: EIFFELTEST_CLIENT_SOCKET): FIXED_STRING

effective function

require

not is_empty(client)

remove (client: EIFFELTEST_CLIENT_SOCKET)

effective procedure

require

not is_empty(client)

ensure

disconnect_is_last: old item(client) = disconnect_item implies is_empty(client)

make

effective procedure

{}

commands: RING_ARRAY[FIXED_STRING]

writable attribute

{}

disconnected_clients: HASHED_SET[EIFFELTEST_CLIENT_SOCKET]

writable attribute

{}

disconnect_item: FIXED_STRING

once function

{}