John Regehr on Nostr: during the course of trying to explain my near-obsession with invariants to my older ...

during the course of trying to explain my near-obsession with invariants to my older kid (a 2nd year CS student), I showed him this code and asked if he could come up with the key loop invariant that results in a strong enough postcondition that we get a proof of correctness, and he got it!

int popcount_kernighan(uint64_t x) {
int c = 0;
while (x) {
x &= x - 1;
c++;
}
return c;
}