Graded Hoare Logic and its Categorical Semantics

TL;DR

This paper introduces Graded Hoare Logic (GHL), a flexible framework that unifies various augmented program logics by incorporating a preordered monoidal analysis through categorical semantics, enabling reasoning about effects and side-effects.

Contribution

It develops a semantic framework using graded categories and fibrations to model GHL, unifying different approaches to augmented program logics within a categorical setting.

Findings

Introduces graded Freyd categories for semantics of GHL

Provides a fibrational model for assertion languages

Unifies various augmented logics under a single framework

Abstract

Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via the paradigm of grading, adapted from the world of functional calculi and semantics. We propose Graded Hoare Logic (GHL), a parameterisable framework for augmenting program logics with a preordered monoidal analysis. We develop a semantic framework for modelling GHL such that grading, logical assertions (pre- and post-conditions) and the underlying effectful semantics of an imperative language can be integrated together. Central to our framework is the notion of a graded category which we extend here, introducing graded Freyd categories which provide a semantics that can interpret many examples of augmented program logics from the literature. We leverage coherent fibrations to model the base assertion language, and thus the overall setting is also fibrational.