On the Completeness of Propositional Hoare Logic
Collections
Author
Kozen, Dexter
Tiuryn, Jerzy
Abstract
We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for Propositional Hoare Logic (PHL): all relationally valid rules {b1}p1{c1}, ..., {bn}pn{cn} --------------------------- {b}p{c} are derivable in PHL, provided the propositional expressiveness conditions are met. Moreover, if the programs pi in the premises are atomic, no expressiveness assumptions are needed.
Date Issued
1999-09
Publisher
Cornell University
Keywords
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR99-1766
Type
technical report