algorithm - 带中断的循环不变量

Question

我试图了解循环不变量如何与中断相互作用。CLRS 3e (pg19) 将循环不变量描述为要求

如果在循环的迭代之前为真，则在下一次迭代之前它仍然为真。

所以给定以下简单的循环

for i = 1 to 5
    if i == 3 then break

可以说i < 4是循环的不变属性吗？论点是，由于循环在break语句处终止，因此在违反该属性后没有迭代。

Answer 1

是的，这将是一个不变量，正是您提到的原因。它是否是有用的不变量是一个单独的问题，取决于您要证明的内容。