The generalization of the Hoarean property of the P program, in the form {]}P{g} , is discussed. -Instead of the Boolean functions in the set of states V , binary relations which are subsets of Vโข where M can be an arbitrary set, are used for I and g, i. It was pointed out in /i/ that for program analysis it is sometimes natural to consider not predicates (Boolean functions) but certain binary relations.
We extend to the binary relations rgumerous concepts and methods which are traditionally connected with predicates on a set of states V . we assume without stipulation that ~ g,h~VXMj where M is the given arbitrary set, and denote the programs (texts in certain languages) by P, Q, R and S. In a deterministic case, p, q, r and s denote the functions P, Q, R and S , compared with the programs; they are defined, and take values in V.
If P is a non-deterministic program then it can be compared with two binary relations p~ and p~ not identical in general, such that p~p~VXV.
We assume that vop#vl exists when and only when, for the initial state v0 the l' program can be concluded and it can give the final state v, . We also assume that vop b u, exists when and only when v~p*v, exists, and for the initial state of v0 the fulfilment of P is for certain completed.
The relation p~ =p'=p is valid for any deterministic P program.
We do not adhere to any rigorously fixed form of description for ], g, h~VXM;
when ],g and h are given by non-deterministic programs we shall understand them as being ~, g* and h +.
The binary relations programs of the products VXV and VX~[ are regarded as manyvalued partial functions in the set I t with their values in V or ~I. Asserting for a certain many-valued function t that t(x)=y (or that I(x)~y~ where x and y are some indicated elements, we shall imply that y is one of the values of the function I , the value of the argument being x(or, that among these values of the function t there is no y ); this could be written as xly (or ~ correspondingly, as ] (xly) ) . Definition i. The P program has the property {]}P{g) if, each time when for certain