在上一个问题中,我寻求帮助编写 apredicate
以查找数字是否为 2 的幂。这是尝试证明以下 C 函数的前奏:
static inline bool
is_power_of_2 (unsigned long v)
{
return v && ((v & (v - 1)) == 0);
}
(这个“技巧”来自这里)。使用我尝试过的前一个谓词:
/*@
ensures positive_power_of_2 (v) <==> \result == \true;
*/
但我使用的各种 SMT 求解器(alt-ergo、z3、gappa、cvc4)似乎都无法证明这一点。