Refinement algebras are abstract algebras for reasoning about programs in a total-correctness framework. We extend a reduct
of von Wright’s demonic refinement algebra with two operators for modelling enabledness and termination of programs. We show
how the operators can be used for expressing relations between programs and apply the algebra to reasoning about action systems.