jam*_*her 1 language-agnostic verification logic variant
参考完全正确性的while规则,WP似乎告诉我,只要找到严格减少的循环变量就足以证明终止.我不能接受,要么是因为我遗漏了某些东西,要么是规则错了.考虑
int i = 1000;
while(true) i--;
其中变量的值i是严格减少的循环变量,但循环当然不会终止.
当然规则需要有一个额外的前提条件,例如i <0→¬B(其中B是公理模式中的循环条件),这样循环条件最终"捕获"循环变量并退出.
还是我错过了什么？