如何解决Hoare逻辑:严格减少循环变量本身如何证明终止?
| 关于完全正确的while规则,WP似乎告诉我,仅找到严格减少的循环变量就足以证明终止。我不能接受,因为我遗漏了一些东西或规则是错误的。考虑int i = 1000;
while(true) i--;
其中变量i
的值是严格递减的循环变量,但循环肯定不会终止。
当然,该规则需要具有其他先决条件,例如i <0→¬B(其中B是公理模式中的循环条件),以便循环条件最终“捕捉”到循环变量并退出。
还是我错过了什么?
解决方法
循环变量必须是自然数。自然数不能减少到零以上。用大的话来说,循环变量是一个相对于良好关系单调递减的值。这是您推理中缺乏的充分根据。
, 如Wikipedia文章所述:
[...]条件B必须暗示t为
不是其范围的最小要素,
否则本规则的前提
会是错误的。
在当前情况下,B为
true
,t为i
。 true
与i
的极小值无关,因此不满足规则的前提。
, 通常的顺序\“ <\”是基于自然数的,而不是整数。为了使关系有充分的基础,其域的每个非空子集都必须具有最小元素。由于可以证明相对于良好关系而言,没有无限的下降链,因此具有变体的循环必须终止。
当然,在最小元素的情况下,循环的条件必须为假!
但是,变体不必限于自然数。超限序也井井有条。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。