A relational division operator: The conjugate kernel (Q2367540)

A binary operator on relations, called conjugate kernel, is introduced. It is defined as a restriction of a residual and behaves as a kind of inverse of the relational product operator. It is shown how relational algebraic methods can be useful in describing fundamental concepts of programming. The conjugate kernel operator is related with Hoare's weakest pre- and postspecification, Joseph's weakest pre- and postspecification, and Dijkstra's weakest precondition. For example, it is proven that, if there exists a solution of the weakest prespecification problem, the conjugate kernel describes an optimal solution. Furthermore, the connection between the conjugate kernel operator and the notion of program correctness is discussed and the use of conjugate kernels in program construction is demonstrated. Finally, the results are compared with other studies of division-like operators for binary relations.