环路终止条件

这些for循环是算法形式正确性证明的第一个基本例子.它们具有不同但等效的终止条件:

1   for ( int i = 0; i != N; ++i )

2   for ( int i = 0; i < N; ++i )

后置条件中的区别变得明显:

第一个给出i == N了循环终止后的有力保证.

第二个只给出了i >= N在循环终止后的弱保证,但你会想到这一点i == N.

如果由于任何原因将增量++i更改为类似的内容i += 2,或者如果i在循环内部进行了修改,或者如果N是负数,则程序可能会失败:

第一个可能陷入无限循环.它在出现错误的循环中提前失败.调试很简单.

第二个循环将终止,并且稍后由于您的错误假设,程序可能会失败i == N.它可能会远离导致错误的循环失败,从而难以追溯.或者它可以默默地继续做一些意想不到的事情,这更糟糕.

您更喜欢哪种终止条件,为什么？还有其他考虑因素吗？为什么许多知道这一点的程序员拒绝应用它？