title: Hoare Logic Loop Invariant
body: <p>I'm looking at Hoare Logic and I'm having problems understanding the method of finding the loop invariant.</p>
  
  <p>Can someone explain the method used to calculate the loop invariant?</p>
  
  <p>And what should a loop invariant should contain to be a "useful" one?</p>
  
  <p>I'm only dealing with simple examples, finding invariants and proving partial and complete correction in examples like:</p>
  
  <pre><code>{ i ≥ 0 } while i &gt; 0 do i := i−1 { i = 0 }
  </code></pre>