+
Point of view
All features
class THREAD_CONTEXT [R_, T_ -> TUPLE]
Summary
Direct parents
Insert list: ANY
Class invariant
Overview
Creation features
{THREAD}
  • make (t: THREAD[R_, T_], a: T_)
Features
{ANY}
{THREAD}
{THREAD}
thread: THREAD[R_, T_]
writable attribute
{ANY}
args: T_
writable attribute
{ANY}
wait
{ANY}
Wait for the thread to finish
require ensure
is_started: BOOLEAN
writable attribute
{ANY}
True if the thread did actually start
is_finished: BOOLEAN
writable attribute
{ANY}
True when the thread has finished
require
status: R_
writable attribute
{ANY}
The returning value
run
require
make (t: THREAD[R_, T_], a: T_)
effective procedure
require
  • t /= Void
  • a /= Void
ensure
native_data: POINTER
writable attribute