Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
int log(int x)
//@requires x >= 1;
//@ensures \result >= 0;
//@ensures (1 << \result) <= x;
{ int r = 0;
int y = x;
while (y > 1)
//@loop_invariant y >= 1 && r >= 0;
//@loop_invariant y * (1 << r) <= x;
{
y = y / 2;
//@assert r < x;
r = r + 1;
}
return r;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment