title: Loop termination conditions
body: <p>These <code>for</code>-loops are among the first basic examples of formal correctness proofs of algorithms. They have different but equivalent termination conditions:</p>
  
  <pre><code>1   for ( int i = 0; i != N; ++i )
  
  2   for ( int i = 0; i &lt; N; ++i )
  </code></pre>
  
  <p>The difference becomes clear in the postconditions:</p>
  
  <ul>
  <li><p>The first one gives the strong guarantee that <code>i == N</code> after the loop terminates.</p></li>
  <li><p>The second one only gives the weak guarantee that <code>i &gt;= N</code> after the loop terminates, but you will be tempted to assume that <code>i == N</code>.</p></li>
  </ul>
  
  <p>If for any reason the increment <code>++i</code> is ever changed to something like <code>i += 2</code>, or if <code>i</code> gets modified inside the loop, or if <code>N</code> is negative, the program can fail:</p>
  
  <ul>
  <li><p>The first one may get stuck in an infinite loop. It fails early, in the loop that has the error. Debugging is easy.</p></li>
  <li><p>The second loop will terminate, and at some later time the program may fail because of your incorrect assumption of <code>i == N</code>. It can fail far away from the loop that caused the bug, making it hard to trace back. Or it can silently continue doing something unexpected, which is even worse.</p></li>
  </ul>
  
  <p>Which termination condition do you prefer, and why? Are there other considerations? Why do many programmers who know this, refuse to apply it?</p>