5. Nondeterminism

Definitions

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

1. The compiler can directly translate the source code into a concurrent implementation.
2. Implementation gains potentially significantly in performance.
3. 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

1. 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

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