A general framework for sound and complete Floyd-Hoare logics

DOI10.1145/1614431.1614438MaRDI QIDQ2946594zbMATHOpenAlexWikidataFDO

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)

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

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)

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).

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

Cited in

(8)

• A Hoare logic for linear systems
• scientific article; zbMATH DE number 553883 (Why is no real title available?)
• A remark on propositional Kripke frames sound for intuitionistic logics
• Fifty years of Hoare's logic
• Indexed and fibered structures for partial and total correctness assertions
• scientific article; zbMATH DE number 1678378 (Why is no real title available?)
• Hoare Logic in the Abstract
• Weakest precondition reasoning for expected run-times of probabilistic programs

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)