Analysis of programs and binary relations

The generalization of the Hoarean property of the Pprogram, in the form $\{f\}P\{g\}$, is discussed. Instead of the Boolean functions in the set of states $V$, binary relations which are subsets of $V\times M$, where $M$ can be an arbitrary set, are used for $f$ and $g$.