On the completeness of propositional Hoare logic

被引：14
|
作者：
Kozen, D [1 ]
Tiuryn, J
机构：
[1] Cornell Univ, Dept Comp Sci, Ithaca, NY 14853 USA
[2] Warsaw Univ, Inst Informat, PL-02097 Warsaw, Poland
来源：
INFORMATION SCIENCES | 2001年 / 139卷 / 3-4期
关键词：
D O I：
10.1016/S0020-0255(01)00164-5
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
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 {b(1)}p(1){c(1)},...,{b(n)}p(n){c(n)} / {b}p{c} are derivable in PHL, provided the propositional expressiveness conditions are met. Moreover, if the programs p; in the premises are atomic, no expressiveness assumptions are needed. (C) 2001 Elsevier Science Inc. All rights reserved.
引用
收藏
页码：187 / 195
页数：9
相关论文
共 50 条
12345