title: Proving an algorithm's correctness in determining the number of 1 bits in a bit string
body: <pre><code>procedure bit count(S: bit string)
  count := 0
        while S != 0
            count := count + 1
            S := S ∧ (S − 1)
  return count {count is the number of 1s in S}
  </code></pre>
  
  <p>Here S-1 is the bit string obtained by changing the rightmost 1 bit of S to a 0 and all the 0 bits to right of this to 1s.</p>
  
  <p>So I understand why this is correct, and I have write a rough explanation;</p>
  
  <p>After every iteration, the rightmost 1 bit in S, as well as all the bits to the right of it, is set equal to 0. Thus, after each iteration, the next right-most 1 is accounted for and set to 0, until the entire string is 0's and the loop breaks with the count equal to the number of 1's. </p>
  
  <p>I know this kind of answer won't pass in any mathematics community, so I was hoping to write a formal proof, but I don't know how to go about doing that.  My proof skills are particularly shoddy, so an explanation of the techniques involved would be greatly appreciated.</p>