Анализ программ и бинарные отношения

Рассматривается обобщение хооровского свойства программы $P$, имеющего вид $\{f\}P\{g\}$: в качестве $f$ и $g$ привлекаются не булевы функции на множестве состояний $V$, а бинарные отношения, являющиеся подмножествами $V\times M$, где $M$ может быть произвольным множеством.