A General Framework for Sound and Complete Floyd-Hoare Logics

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

doi:10.1145/1614431.1614438

A General Framework for Sound and Complete Floyd-Hoare Logics

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

School of Informatics

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English
Article number	7
Pages (from-to)	7:1-7:31
Number of pages	31
Journal	ACM Transactions on Computational Logic
Volume	11
Issue number	1
DOIs	https://doi.org/10.1145/1614431.1614438
Publication status	Published - Oct 2009

Keywords / Materials (for Non-textual outputs)

Hoare logic
stream circuits
traced monoidal categories

Access to Document

10.1145/1614431.1614438

http://doi.acm.org/10.1145/1614431.1614438

Cite this

@article{64deb385249145439ad1ffa38c6eb12a,

title = "A General Framework for Sound and Complete Floyd-Hoare Logics",

abstract = "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).",

keywords = "Hoare logic, stream circuits, traced monoidal categories",

author = "Rob Arthan and Ursula Martin and Mathiesen, {Erik A.} and Paulo Oliva",

year = "2009",

month = oct,

doi = "10.1145/1614431.1614438",

language = "English",

volume = "11",

pages = "7:1--7:31",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "ACM",

number = "1",

}

TY - JOUR

T1 - A General Framework for Sound and Complete Floyd-Hoare Logics

AU - Arthan, Rob

AU - Martin, Ursula

AU - Mathiesen, Erik A.

AU - Oliva, Paulo

PY - 2009/10

Y1 - 2009/10

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

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

KW - Hoare logic

KW - stream circuits

KW - traced monoidal categories

U2 - 10.1145/1614431.1614438

DO - 10.1145/1614431.1614438

M3 - Article

SN - 1529-3785

VL - 11

SP - 7:1-7:31

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 1

M1 - 7

ER -

A General Framework for Sound and Complete Floyd-Hoare Logics

Abstract

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this