Demonic Algebra with Domain

We first recall the concept of Kleene algebra with domain (KAD). Then we explain how to use the operators of KAD to define a demonic refinement ordering and demonic operators (many of these definitions come from the literature). Then, taking the properties of the KAD-based demonic operators as a guideline, we axiomatise an algebra that we call Demonic algebra with domain (DAD). The laws of DAD not concerning the domain operator agree with those given in the 1987 CACM paper Laws of programming by Hoare et al. Finally, we investigate the relationship between demonic algebras with domain and KAD-based demonic algebras. The question is whether every DAD is isomorphic to a KAD-based demonic algebra. We show that it is not the case in general. However, if a DAD $\mathcal{D}$ is isomorphic to a demonic algebra based on a KAD $\mathcal{K}$, then it is possible to construct a KAD isomorphic to $\mathcal{K}$ using the operators of $\mathcal{D}$. We also describe a few open problems.