  Composition and demonic refinement $\sqsubseteq$ of binary relations are
defined by \begin{align*} (x, y)\in (R;S)&\iff \exists z((x, z)\in R\wedge (z,
y)\in S)
  R\sqsubseteq S&\iff (dom(S)\subseteq dom(R) \wedge
R\restriction_{dom(S)}\subseteq S)
  \end{align*} where $dom(S)=\{x:\exists y (x, y)\in S\}$ and
$R\restriction_{dom(S)}$ denotes the restriction of $R$ to pairs $(x, y)$ where
$x\in dom(S)$.
  Demonic calculus was introduced to model the total correctness of
non-deterministic programs and has been applied to program verification.
  We prove that the class $R(\sqsubseteq, ;)$ of abstract $(\leq, \circ)$
structures isomorphic to a set of binary relations ordered by demonic
refinement with composition cannot be axiomatised by any finite set of
first-order $(\leq, \circ)$ formulas. We provide a fairly simple, infinite,
recursive axiomatisation that defines $R(\sqsubseteq, ;)$. We prove that a
finite representable $(\leq, \circ)$ structure has a representation over a
finite base. This appears to be the first example of a signature for binary
relations with composition where the representation class is non-finitely
axiomatisable, but where the finite representations for finite representable
structures property holds.
