+
Point of view
EVENT_DESCRIPTOR
class EVENTS_SET
require
- file /= Void
- file.is_connected
- file.has_descriptor
- not queryable
require
- file /= Void
- file.is_connected
- file.has_descriptor
- queryable
require
- file /= Void
- file.is_connected
- file.has_descriptor
- not queryable
require
- file /= Void
- file.is_connected
- file.has_descriptor
- queryable
ensure
-
equivalence: Result = a_event.expected(Current)