Proof system for weakest prespecification (Q1104780)

\textit{C. A. R. Hoare} and \textit{He Jifeng} [Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 9, 51-84 (1986; Zbl 0603.68009)] introduced the notions of weakest prespecification and weakest postspecification within the framework of the calculus of binary relations, and the relational representation of specifications is compared with Dijkstra's programming language and VDM representation. For relations \(Q\subseteq Y\times Z\) and \(R\subseteq X\times Z\), the weakest prespecification of Q to achieve R is the greatest relation \(P\subseteq X\times Y\) such that P composed with Q is included in R. Similarly, for relations \(P\subseteq X\times Y\) and \(R\subseteq X\times Z\), the weakest postspecification of P to achieve R is the greatest relation \(Q\subseteq Y\times Z\) such that P composed with Q is included in R. The purpose of the present paper is to define a logic based on calculus of relations augmented with operations of weakest prespecification and weakest postspecification and to give a deduction method for the logic. Formulas of the logic are intended to represent statements of the form: a pair of objects is a member of a relation. A true formula corresponding to a relation R represents the fact that R coincides with a universal relation. Entailment of the form: if relations \(R_ 1,...,R_ n\) are universal, then a relation R is universal, can also be expressed in the language. Formulas of the language enable us to express many other important properties which ca be formulated in terms of equality or inclusion of relations. The logic is an extension of the system introduced by the author [Pr. Inst. Podstaw Inf. Pol. Akad. Nauk 543 (1984; Zbl 0553.68053)] and investigated by \textit{W. Buszkowski} and the author [Bull. Pol. Acad. Sci., Math. 34, 345-354 (1986; Zbl 0618.68078)].