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

| 关于完全正确的while规则，WP似乎告诉我，仅找到严格减少的循环变量就足以证明终止。我不能接受，因为我遗漏了一些东西或规则是错误的。考虑

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

其中变量

i

的值是严格递减的循环变量，但循环肯定不会终止。 当然，该规则需要具有其他先决条件，例如i <0→¬B（其中B是公理模式中的循环条件），以便循环条件最终“捕捉”到循环变量并退出。 还是我错过了什么？