A General Framework for Sound and Complete Floyd-Hoare Logics

TL;DR

This paper introduces a highly general framework for Hoare logics using traced symmetric monoidal categories, enabling unified reasoning about various systems and extending traditional Hoare logic to new contexts.

Contribution

It generalizes Hoare logic through category theory, providing a versatile abstraction applicable to diverse systems and enabling the development of new Hoare logics.

Findings

Unified framework for Hoare logics via category theory

Examples include partial correctness of programs and pointer programs

Case studies on run-time analysis and stream circuits

Abstract

This paper presents an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into the category of pre-orders and monotone relations. We give several examples of how our theory generalises usual Hoare logics (partial correctness of while programs, partial correctness of pointer programs), and provide some case studies on how it can be used to develop new Hoare logics (run-time analysis of while programs and stream circuits).