A relation algebraic model of robust correctness

AbstractWe propose a new and uniform abstract relational approach to demonic nondeterminism and robust correctness similar to Hoare's chaos semantics. It is based on a specific set of relations on flat lattices. This set forms a complete lattice. Furthermore, we deal with the refinement of programs. Among other things, we show the correctness of the unfold/fold method for demonic nondeterminism and robust correctness as refinement relation and investigate relationships to Dijkstra's wp-calculus and Morgan's specification statement