Added feature comments.
Added missing postconditions.
This commit is contained in:
@@ -16,12 +16,16 @@ inherit
|
|||||||
feature -- Access
|
feature -- Access
|
||||||
|
|
||||||
started: BOOLEAN
|
started: BOOLEAN
|
||||||
|
-- is the server started?
|
||||||
|
|
||||||
stopped: BOOLEAN
|
stopped: BOOLEAN
|
||||||
|
-- is the server stoped?
|
||||||
|
|
||||||
terminated: BOOLEAN
|
terminated: BOOLEAN
|
||||||
|
-- is the server terminated?
|
||||||
|
|
||||||
port: INTEGER
|
port: INTEGER
|
||||||
|
-- Server listening on port.
|
||||||
|
|
||||||
feature -- Event
|
feature -- Event
|
||||||
|
|
||||||
@@ -29,17 +33,24 @@ feature -- Event
|
|||||||
do
|
do
|
||||||
started := True
|
started := True
|
||||||
port := a_port
|
port := a_port
|
||||||
|
ensure then
|
||||||
|
started_set: started = True
|
||||||
|
port_set: port = a_port
|
||||||
end
|
end
|
||||||
|
|
||||||
on_stopped
|
on_stopped
|
||||||
do
|
do
|
||||||
stopped := True
|
stopped := True
|
||||||
|
ensure then
|
||||||
|
stopped_set: stopped = True
|
||||||
end
|
end
|
||||||
|
|
||||||
on_terminated
|
on_terminated
|
||||||
do
|
do
|
||||||
port := 0
|
port := 0
|
||||||
terminated := True
|
terminated := True
|
||||||
|
ensure then
|
||||||
|
terminated_set: terminated = True
|
||||||
end
|
end
|
||||||
|
|
||||||
note
|
note
|
||||||
|
|||||||
Reference in New Issue
Block a user