  Demonic composition, demonic refinement and demonic union are alternatives to
the usual "angelic" composition, angelic refinement (inclusion) and angelic
(usual) union defined on binary relations. We first motivate both the angelic
and demonic via an analysis of the behaviour of non-deterministic programs,
with the angelic associated with partial correctness and demonic with total
correctness, both cases emerging from a richer algebraic model of
non-deterministic programs incorporating both aspects. Zareckii has shown that
the isomorphism class of algebras of binary relations under angelic composition
and inclusion is finitely axiomatised as the class of ordered semigroups. The
proof can be used to establish that the same axiomatisation applies to binary
relations under demonic composition and refinement, and a further modification
of the proof can be used to incorporate a zero element representing the empty
relation in the angelic case and the full relation in the demonic case. For the
signature of angelic composition and union, it is known that no finite
axiomatisation exists, and we show the analogous result for demonic composition
and demonic union by showing that the same axiomatisation holds for both. We
show that the isomorphism class of algebras of binary relations with the
"mixed" signature of demonic composition and angelic inclusion has no finite
axiomatisation. As a contrast, we show that the isomorphism class of partial
algebras of binary relations with the partial operation of constellation
product and inclusion (also a "mixed" signature) is finitely axiomatisable.
