5.|5. Nondeterminism 5.Nondeterminism

Definitions
【5.|5. Nondeterminism】Non-determinism in design: a property of a computation which may have more than one result.
Non-determinism in interaction: A property of the operation environment which may lead to different sequences of concurrent stimuli.
Advantage

The compiler can directly translate the source code into a concurrent implementation.
Implementation gains potentially significantly in performance.
The programmer do not need to handle any of the details of a concurrent implementation

Implementation form in Ada
Select_statement: selective_accept, conditional_entry-call, time_entry, asynchronous_select

selective_accept
First: select-accept
Second:select-guarded-accept
Third:select-guarded-accept-delay
Fourth:select-guard-accept-terminate
Fifth:select-guard-accept-else

Correctness of non-deterministic program

Correctness predicates needs to hold true irrespective of the actual sequence of interaction point.
Correctness predicates needs to hold true for all possible sequence of interaction point.