A general framework for sound and complete Floyd-Hoare logics

DOI10.1145/1614431.1614438zbMATH Open1351.03020arXiv0807.1016OpenAlexW2084929300WikidataQ55393275 ScholiaQ55393275MaRDI QIDQ2946594FDOQ2946594

Authors: Rob Arthan, Erik A. Mathiesen, Paulo Oliva, Ursula Martin Webb 

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: This paper presents an abstraction of Hoare logic to traced symmetric monoidal categories, a very general framework for the theory of systems. Our abstraction is based on a traced monoidal functor from an arbitrary traced monoidal category into the category of pre-orders and monotone relations. We give several examples of how our theory generalises usual Hoare logics (partial correctness of while programs, partial correctness of pointer programs), and provide some case studies on how it can be used to develop new Hoare logics (run-time analysis of while programs and stream circuits).

Full work available at URL: https://arxiv.org/abs/0807.1016

Recommendations

• Hoare Logic in the Abstract
• Semantic properties of monotone Floyd-Hoare logics
• A language independent proof of the soundness and completeness of generalized Hoare logic
• Floyd-Hoare logic in iteration theories
• Partial hyperdoctrines: categorical models for partial function logic and Hoare logic

zbMATH Keywords

Hoare logictraced monoidal categoriesstream circuits

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Cited In (8)

• Weakest precondition reasoning for expected run-times of probabilistic programs
• A remark on propositional Kripke frames sound for intuitionistic logics
• Hoare Logic in the Abstract
• Fifty years of Hoare's logic
• Indexed and fibered structures for partial and total correctness assertions
• A Hoare logic for linear systems
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: A general framework for sound and complete Floyd-Hoare logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946594)