Hoare Logic in the Abstract

Ursula Martin, Erik A. Mathiesen, Paulo Oliva

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. We first identify a particular class of functors – which we call ‘verification functors’ – between traced symmetric monoidal categories and subcategories of Preord (the category of preordered sets and monotone mappings). We then give an abstract definition of Hoare triples, parametrised by a verification functor, and prove a single soundness and completeness theorem for such triples. In the particular case of the traced symmetric monoidal category of while programs we get back Hoare’s original rules. We discuss how our framework handles extensions of the Hoare logic for while programs, e.g. the extension with pointer manipulations via separation logic. Finally, we give an example of how our theory can be used in the development of new Hoare logics: we present a new sound and complete set of Hoare-logic-like rules for the verification of linear dynamical systems, modelled via stream circuits.
Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publicationCSL 2006
PublisherSpringerLink
Pages501-515
Number of pages15
DOIs
Publication statusPublished - 2006

Fingerprint

Dive into the research topics of 'Hoare Logic in the Abstract'. Together they form a unique fingerprint.

Cite this