Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic, Incorrectness Logic, and Beyond

TL;DR

This paper explores a unified framework for various program logics, including Hoare and incorrectness logics, by analyzing their properties through the lens of Kleene algebra with top and tests.

Contribution

It introduces a generalized approach connecting Hoare-like triples and Kleene algebras, offering a holistic perspective on program reasoning.

Findings

Comparison of properties across different program logics

Establishment of connections with Kleene algebra with top and tests

Advancement towards a unified theoretical framework

Abstract

We aim at a holistic perspective on program logics, including Hoare and incorrectness logics. To this end, we study different classes of properties arising from the generalization of the aforementioned logics. We compare our results with the properties expressible in the language of Kleene algebra with top and tests.