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