Hoare logic in the abstract

5Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We present an abstraction of Hoare logic to truced 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. © Springer-Verlag Berlin Heidelberg 2006.

Cite

CITATION STYLE

APA

Martin, U., Mathiesen, E. A., & Oliva, P. (2006). Hoare logic in the abstract. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4207 LNCS, pp. 501–515). Springer Verlag. https://doi.org/10.1007/11874683_33

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free