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
the formulas and specify pairs of states. Then, if the pair satisfies , if we run starting from and then once more starting from state , we will obtain a pair of new states that satisfies . Naturally, the formulas and can refer to the variables of either the first or the second state, usually notated by indexing (, ).
This kind of Hoare logic can be used to justify a number of optimizing transformations for imperative programs [Benton 2004].
A probabilistic variant of relational Hoare logic, pRHL, is used in verifying the correctness of cryptographic primitives.
Benton, Nick. 2004. ‘Simple Relational Correctness Proofs for Static Analyses and Program Transformations’. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 14–25. Association for Computing Machinery. https://doi.org/10.1145/964001.964003. [pdf]
@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},
}