0 
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.

4

2 回答 2

1

使用归纳的证明可能如下所示：

声明：n在算法的第 th 次迭代开始时，您已经看到（翻转） n-11（设置）位和count == n-1。

证明：
基础：在第一次迭代中微不足道n==1- 您还没有看到任何设置位，并且 count 设置为 0 ..
假设：对于每个k<n（对于某些n），该声明都是正确的。
证明n：第 n 次迭代之后是n-1迭代。在n-1迭代中，从归纳假设中您已经看到了n-1bits 和count == n-1.
由于您到达n迭代，n-1迭代成功结束 - 因此未满足结束条件，因此有一个翻转位。您还增加count了 1，因此在第nth 步中您翻转了n位和count == n.

从上面我们可以得出结论，当算法结束时，count == #flipped_bits.

量子点

请注意，以上是部分正确性- 它证明如果算法终止 - 它会产生正确的答案，但不保证终止。
可以通过显示最多有|S|步骤来保证终止，因为您可以在大多数时候翻转最正确的位，|S|直到您得到S = 0. （终止+部分正确称为完全正确）

如果您对证明算法感兴趣，您可能会对Hoare Logic感兴趣，它提供了一个正式的工具，用于验证程序是否正确。这个研究领域被称为软件验证。

于 2012-12-05T06:57:03.160 回答
0

首先，这是不正确的。你想要while S != 0，没有while S = 0。

至于证明，我会使用归纳证明：证明如果没有设置位，它可以正常工作，然后证明如果至少设置了一个位，它会增加计数，减少设置的位数一，并重复。

在归纳步骤中，唯一困难的部分是表明在 之后S := S ∧ (S − 1)，在 S 中设置的位数将减少 1。主要部分是对于任何形式的数字 N，其10..0形式N-1为01..1-这就是二进制计数的基本性质。不过，我可能会反过来做——表明对于任何数字 : 01..1，下一个连续数字是10..0，基本上归结为：“1+1 -> 0 + 进位”。

于 2012-12-05T06:33:50.370 回答