Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
复制标题
DOI：
10.1145/322108.322121
复制
发表时间：
1979
期刊：
影响因子：
--
通讯作者：
E. Clarke
中科院分区：
文献类型：
--
作者：
E. Clarke
Hoare公理系统用于建立程序的部分正确性可能是不完整的，因为（a）断言语言相对于底层解释的不完整性或（B）断言语言无法表达循环的mvanant Cook已经表明，如果断言语言有一个完整的证明系统，（l e断言语言的所有真公式）如果断言语言满足一个自然的可表达性条件，那么就可以为Algol的一个大子集设计一个可靠而完整的公理系统。即使在Cook的这种特殊意义下，也不可能得到健全的完备的Hoare公理集。这些结构包括：（0）在使用静态作用域的ldenuifiers的程序设计语言中的带过程参数的递归过程和（u）在允许无参数递归过程的语言中的coroutmes。
Hoare axiom systems for establishing partial correctness of programs may fail to be complete because of (a) incompleteness of the assertion language relative to the underlying interpretation or (b) inability of the assertion language to express the mvanants of loops Cook has shown that if there IS a complete proof system for the assertion language (l e all true formulas of the assertion language) and if the assertion language satisfies a natural expresstbthty condition then a sound and complete axiom system for a large subset of Algol may be devised We exhibit programming language constructs for which it ms impossible to obtain sound and complete sets of Hoare axioms even in this special sense of Cook's These constructs include (0 recursive procedures with procedure parameters in a programming language which uses static scope of ldenufiers and (u) coroutmes in a language which allows parameterless recurslve procedures Modifications of these constructs for which sound and complete systems of axioms may be obtained are also discussed