Demonic nondeterminism is a type of nondeterminism in which the "worst" possible action will be chosen.
The definition of "worst" depends on the setting.
In a functional programming language with nondeterminism, a demonic implementation will implement a nondeterministic choice by preferentially resolving to the branch that will cause nontermination.
For example, when faced with the nondeterministic choice
it will always pick .
In domain theory, (locally) demonic nondeterminism is modelled using the Smyth powerdomain.
[Søndergaard and Sestoft 1992] report that the domain-theoretic point of view may only model global demonic nondeterminism, as
a fixed-point theoretic characterization of these kinds of semantics is very difficult and still under investigation
When reasoning with Hoare logic and weakest preconditions, the operator implements demonic nondeterministic choice when
Thus, for the nondeterministic choice to be "safe," both the preconditions of and must hold.
Søndergaard, H., and P. Sestoft. 1992. ‘Non-Determinism in Functional Languages’. The Computer Journal 35 (5): 514–23. https://doi.org/10.1093/comjnl/35.5.514.
@article{sondergaard_1992,
title = {Non-determinism in {Functional} {Languages}},
volume = {35},
doi = {10.1093/comjnl/35.5.514},
number = {5},
journal = {The Computer Journal},
author = {Søndergaard, H. and Sestoft, P.},
year = {1992},
pages = {514--523}
}
Broy, M., and M. Wirsing. 1981. ‘On the Algebraic Specification of Nondeterministic Programming Languages’. In CAAP ’81, edited by Egidio Astesiano and Corrado Böhm, 112:162–79. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-10828-9_61.
@inproceedings{broy_1981,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {On the algebraic specification of nondeterministic programming languages},
volume = {112},
doi = {10.1007/3-540-10828-9_61},
booktitle = {{CAAP} '81},
publisher = {Springer Berlin Heidelberg},
author = {Broy, M. and Wirsing, M.},
editor = {Astesiano, Egidio and Böhm, Corrado},
year = {1981},
pages = {162--179}
}