EMBEDDING A DEMONIC SEMILATTICE IN A RELATION ALGEBRA

We present a refinement ordering between binary relations, viewed as p rograms or specifications, This ordering induces a complete join semil attice that can be embedded in a relation algebra, This embedding then allows an easy proof of many properties of the refinement semilattice , by making use of the well-known corresponding properties of relation algebras. The operations of the refinement semilattice corresponding to join and composition in the embedding algebra are, respectively, de monic join and demonic composition. The weakest prespecification and p ostspecification operators of Hoare and He, defined over a relation al gebra, also have corresponding operators in the semilattice.