Remark. Angelic nondeterminism [dt-0063]

Consider the following three programs:

  1. x := 1
  2. \textsf {while}\ \textsf {true}\ \textsf {do}\ \textsf {skip}
  3. \textsf {while}\ \textsf {true}\ \textsf {do}\ \textsf {skip}\ \textsf {od} + x := 1
Given a state \sigma , let \sigma ' = \sigma (x \mapsto 1). Then, the possible results of these programs are \{ \sigma ' \}, \{ \bot \}, and \{\sigma ', \bot \} respectively. Because the Hoare construction identifies \approx _H-equivalent sets, the Hoare powerdomain semantics will consider programs 1 and 3 to be the same. That is, the non-determinism is angelic. The bad outcome (\bot ) is only said to happen if it is inevitable.