A relational division operator: The conjugate kernel (Q2367540): Difference between revisions
From MaRDI portal
Latest revision as of 18:28, 17 May 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A relational division operator: The conjugate kernel |
scientific article |
Statements
A relational division operator: The conjugate kernel (English)
0 references
19 January 1994
0 references
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.
0 references
relation algebra
0 references
relational division operator
0 references
axiomatic semantics
0 references
weakest precondition
0 references
weakest prespecification
0 references
program correctness
0 references
program construction
0 references