Relational Hoare logic

Relational Hoare logic (or, more appropriately, Benton logic) is a form of Hoare logic whose precondition and postcondition are not simply predicates, but relations.

If we are working with binary relations, in the usual proposition

\{ \phi \}\ P\ \{ \psi \}

the formulas \phi and \psi specify pairs of states. Then, if the pair (s_1, s_2) satisfies \phi, if we run P starting from s_1 and then once more starting from state s_2, we will obtain a pair of new states (s'_1, s'_2) that satisfies \psi. Naturally, the formulas \phi and \psi can refer to the variables of either the first or the second state, usually notated by indexing (x_1, x_2).

This kind of Hoare logic can be used to justify a number of optimizing transformations for imperative programs Benton 2004.

In cryptographic code

A probabilistic variant of relational Hoare logic, pRHL, is used in verifying the correctness of cryptographic primitives.

References

• RHL/Benton logic was introduced in the following POPL 2004 paper:

@inproceedings{benton_2004,
	title = {Simple Relational Correctness Proofs for Static Analyses and Program Transformations},
	doi = {10.1145/964001.964003},
	pages = {14--25},
	booktitle = {Proceedings of the 31st {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
	publisher = {Association for Computing Machinery},
	author = {Benton, Nick},
	date = {2004},
}