A General Framework for Sound and Complete Floyd-Hoare Logics

Rob Arthan, Ursula Martin, Erik A. Mathiesen, Paulo Oliva

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

This article 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 preorders and monotone relations. We give several examples of how our theory generalizes 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 (runtime analysis of while programs and stream circuits).
Original languageEnglish
Article number7
Pages (from-to)7:1-7:31
Number of pages31
JournalACM Transactions on Computational Logic
Volume11
Issue number1
DOIs
Publication statusPublished - Oct 2009

Keywords / Materials (for Non-textual outputs)

  • Hoare logic
  • stream circuits
  • traced monoidal categories

Fingerprint

Dive into the research topics of 'A General Framework for Sound and Complete Floyd-Hoare Logics'. Together they form a unique fingerprint.

Cite this