4
$\begingroup$
   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} 

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.

So I understand why this is correct, and I have write a rough explanation;

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.

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.

  • 0
    Is ^ and or xor?2012-12-05
  • 1
    @copper.hat: It has to be $\land$ for the algorithm to work.2012-12-05

3 Answers 3