Sciweavers

CORR
2008
Springer

A General Framework for Sound and Complete Floyd-Hoare Logics

13 years 3 months ago
A General Framework for Sound and Complete Floyd-Hoare Logics
er presents an abstraction of Hoare logic to traced symmetric monoidal categories, a eral 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). Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms: Hoare logic, traced monoidal categories Additional Key Words and Phrases: Stream circuits
Rob Arthan, Ursula Martin, Erik A. Mathiesen, Paul
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Rob Arthan, Ursula Martin, Erik A. Mathiesen, Paulo Oliva
Comments (0)