We give an algebraic model of the designs of UTP based on a variant of modal semirings, hence generalising the original relational
model. This is intended to exhibit more clearly the algebraic principles behind UTP and to provide deeper insight into the
general properties of designs, the program and specification operators, and refinement. Moreover, we set up a formal connection
with general and total correctness of programs as discussed by a number of authors. Finally we show that the designs form
a left semiring and even a Kleene and omega algebra. This is used to calculate closed expressions for the least and greatest
fixed-point semantics of the demonic while loop that are simpler than the ones obtained from standard UTP theory and previous
algebraic approaches.