Inadequacy of computable loop invariants
Inadequacy of computable loop invariants
复制标题
可计算循环不变量的不足
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Y. Gurevich
中科院分区：
文献类型：
--
作者：
A. Blass;Y. Gurevich
Hoare逻辑是一种被广泛推荐的验证工具。然而，这里有一个查找容易检查的循环不变量的问题；众所周知，可判定断言不足以验证while程序，即使前置条件和后置条件是可判定的。我们在这里展示了一个更强的结果：可决定不变量不足以验证单循环程序。我们还表明，即使在极其简单的情况下，这个问题也会出现。设<斜体>N</斜体>是自然数集合与函数<斜体>S(x)</斜体>=<斜体>x</斜体>+1,<斜体>D(x)</斜体>=2<斜体>(x)</斜体>=***<斜体>x</斜体>/2***组成的结构。有一个单循环程序***只使用三个变量<italic>x,y,z</italic>，使得断言的程序<italic>x</italic>=<italic>y</italic>=<italic>z</italic>=0 *** false在<italic>N</italic>上部分正确，但是任何循环不变式<italic>I（x,y,z）对于这个断言的程序是不可判定的。
Hoare logic is a widely recommended verification tool. There is, however, a problem of finding easily checkable loop invariants; it is known that decidable assertions do not suffice to verify while programs, even when the pre- and postconditions are decidable. We show here a stronger result: decidable invariants do not suffice to verify single-loop programs. We also show that this problem arises even in extremely simple contexts. Let <italic>N</italic> be the structure consisting of the set of natural numbers together with the functions <italic>S(x)</italic>=<italic>x</italic>+1,<italic>D(x)</italic>=2<italic>(x)</italic>=***<italic>x</italic>/2***. There is a single-loop program *** using only three variables <italic>x,y,z</italic> such that the asserted program <italic>x</italic>=<italic>y</italic>=<italic>z</italic>=0 *** false is partially correct on <italic>N</italic> but any loop invariant <italic>I(x,y,z) for this asserted program is undecidable.