Hoare逻辑：严格降低循环变量本身如何证明终止？

参照while rule for total correctness，WP似乎告诉我，找到严格减少的循环变体足以证明终止。我无法接受，因为我错过了某些东西或者规则是错误的。考虑Hoare逻辑：严格降低循环变量本身如何证明终止？

int i = 1000; 
while(true) i--;

其中变量i的值是严格递减的循环变种，但环肯定不会终止。

当然规则需要有一个附加的先决条件，如事我< 0→¬B（其中乙处于公理模式循环条件），使得循环条件最终“捕获”循环变并退出。

或者我错过了什么？

来源

2011-05-31 jameshfisher

循环变量必须是自然数。自然数不能减少过零。使用大词汇，循环变体是一个相对于有根的关系单调递减的值。这是你的推理所缺少的有根有据。

来源

2011-05-31 15:12:52

或者换句话说，'i'并不是我认识的任何语言的严格递减变体 - 在大多数情况下，它会达到最小值，然后绕回（即变大）或触发未定义的行为（可能会终止循环，你永远不知道）。也许在某些真实的情况下，假设我们可以认为'int'是某种语言中的一个bignum，在这种情况下n.m.的完整解释是必需的 - 它正在减少，但对于一个良好的秩序而言不是。 – 2011-05-31 15:33:18

@Steve它也不一定，请参阅[bignum]（http://en.wikipedia.org/wiki/Bignum）。如果你有一台Linux机器，在终端上键入'bc'。在那里，你有一种无限精确的编程语言在你的指尖。 – 2011-05-31 15:39:17

非常简单的答案，谢谢你。 – jameshfisher 2011-05-31 16:12:54

作为维基百科文章中指出：

[...]的条件乙必须暗示吨是不是它的范围，的最小元件对本否则前提规则将是错误的。

在手边的情况下，乙是true和吨是i。 true对i的最小性没有影响，所以不符合规则的前提。

来源

2011-05-31 17:55:50 WReach

你引用的文本暗示了变量从一次迭代到下一次迭代严格减少，这不在OP的例子中。（根据语言，OP的例子调用UB或在某个步骤增加2^32-1。） – 2011-06-08 00:56:22

通常的排序“<”在自然数上是有根据的，但不是整数。为了使关系有根据，其域的每个非空子集必须具有最小元素。既然可以证明，关于一个有根的关系没有无限下降链，那么带有变体的循环必须终止。

当然，在最小元素的情况下，循环的条件必须是假的！

然而，变体不需要限制在自然数。超限定序也是有序的。

来源

2011-08-18 05:06:51 JustinL

Hoare逻辑：严格降低循环变量本身如何证明终止？

回答

相关问题