In a previous paper[1], the authors defined a specification language C within the complete lattice of monotonic predicate transformers using only simple primitive commands and functional composition in addition to meets and joins. It was shown in that paper that all monotonic predicate transformers can be generated in this language.

This paper continues the work of the previous paper and focuses on the duality between angelic and demonic nondeterminism together with the duality between nondetermination and miracles. The paper considers several such languages of the command lattice, showing how they are interrelated and how they can be constructed. Finally, although many of the sublanguages are complete lattices, it is shown that the language of nonmiraculous conjunctive commands (that is, the language in which Dijkstra’s guarded commands are embedded) has a more irregular structure.

This paper is a significant continuation of the previous work, and the authors obviously plan further papers on this topic.