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}
这里的S-1是将S最右边的1位变为0，右边的0位全部变为1得到的位串。
所以我明白为什么这是正确的，我写了一个粗略的解释；
在每次迭代之后，S 中最右边的 1 位以及它右边的所有位都设置为 0。因此，在每次迭代之后，下一个最右边的 1 被考虑并设置为0，直到整个字符串为 0 且循环中断且计数等于 1 的数量。
我知道这种答案不会在任何数学社区通过，所以我希望写一个正式的证明，但我不知道该怎么做。我的证明技巧特别拙劣，因此非常感谢对所涉及的技术的解释。
最佳答案
使用归纳法的证明可能如下所示:
声明:在n的开头算法的第 th 次迭代，您已经看到(翻转)n-1 1(设置)位和 count == n-1 .
证明:
基础:对于n==1来说微不足道，在第一次迭代中 - 您还没有看到任何设置位，并且计数设置为 0..
假设:对于每个 k<n 的声明都是正确的(对于一些 n )。
n的证明:第n次迭代之后是n-1迭代。在n-1迭代，从你已经看到的归纳假设n-1位和 count == n-1 .
自从你到达n迭代，n-1迭代成功结束 - 因此不满足结束条件，所以有一个翻转位。你还增加了count一个，因此在n你翻转的第 th 步 n位和 count == n .
从上面我们可以得出结论，当算法结束时，count == #flipped_bits .
QED
请注意，以上是部分正确性 - 它证明如果算法终止 - 它会产生正确的答案，但它不能保证终止。
保证终止可以通过显示最多|S|来完成。步骤，因为你最多可以翻转最右边的位 |S|次直到你得到S = 0 . (终止+部分正确称为完全正确)
如果您对证明算法感兴趣，您可能会对 Hoare Logic 感兴趣，它给出了一个正式的工具来验证一个程序是否正确。这一研究领域被称为 Software Verification .
关于algorithm - 证明算法在确定位串中 1 位数方面的正确性，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/13717535/