Hoare Logic in the Abstract

Hoare Logic in the Abstract,10.1007/11874683_33,Ursula Martin,Erik A. Mathiesen,Paulo Oliva

Hoare Logic in the Abstract   (Citations: 1)
BibTex | RIS | RefWorks Download
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 (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.
Conference: Computer Science Logic - CSL , vol. 4207, pp. 501-515, 2006
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...There are theoretical indications that the Floyd-Hoare approach applies to a very wide class of systems indeed [9]...
    • ...Some experimentation has begun in applying the approach of the present paper to other systems (including one of the two main general types identified in [9]) with continuous systems as a goal...

    R. D. Arthan. A Verified Formal Model of a VC Generator

Sort by: