Thirty-seven years of relational Hoare logic: remarks on its principles and history

TL;DR

This paper reviews 37 years of relational Hoare logic, highlighting foundational principles, historical development, and proposing new rules and notions of completeness to unify the field.

Contribution

It provides a historical overview of relational Hoare logic, clarifies core principles, and introduces new proof rules and a notion of completeness.

Findings

Identifies core principles underlying relational Hoare logic

Proposes a new proof rule for relational reasoning

Suggests a new notion of completeness for the logic

Abstract

Relational Hoare logics extend the applicability of modular, deductive verification to encompass important 2-run properties including dependency requirements such as confidentiality and program relations such as equivalence or similarity between program versions. A considerable number of recent works introduce different relational Hoare logics without yet converging on a core set of proof rules. This paper looks backwards to little known early work. This brings to light some principles that clarify and organize the rules as well as suggesting a new rule and a new notion of completeness.