Skip to main content
Kent Academic Repository

Graded Hoare Logic and its Categorical Semantics

Gaboardi, Marco, Katsumata, Shin-ya, Orchard, Dominic, Sato, Tetsuya (2021) Graded Hoare Logic and its Categorical Semantics. European Symposium on Programming 2021, . pp. 234-263. (doi:10.1007/978-3-030-72019-3_9) (KAR id:91713)

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.

Item Type: Article
DOI/Identification number: 10.1007/978-3-030-72019-3_9
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Dominic Orchard
Date Deposited: 24 Nov 2021 10:38 UTC
Last Modified: 29 Nov 2021 10:18 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/91713 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.