abs()返回负数？

#include <stdio.h>
#include <limits.h>
#include <stdlib.h>

int main(void)
{
    printf("%d\n", abs(INT_MIN));
    return 0;
}

你猜，上面的代码会输出什么？提示：用补码能表示最小的32位整数是-2147483648，最大是2147483647。

结果是：

-2147483648

虽然这是未定义的行为，但是求绝对值返回个负数感觉很怪不是吗？

我用sbv实现一个的abs：

import Data.SBV.Bridge.CVC4

abs' n = ite (n .>= 0) n (negate n)

然后在ghci里验证，马上就发现abs'会返回负数：

ghci> prove $ forAll ["x"] $ \(x::SInt64) -> abs' x .>= 0
Falsifiable. Counter-example:
  x = -9223372036854775808 :: SInt64

我以前觉得这些细枝末节是无关紧要的，但现在我很重视程序正确性，遇上这问题要这么办呢？

我是在看Generating Verification Conditions for Whiley（这篇也很有趣）的时候想到这个问题的。

文中的abs实现：

int abs(int x) ensures $ >= 0:
    if x >= 0:
         return x
    else:
         return -x

如果Whiley的int和机器字对应，那么abs就会遇到上面的问题，即ensures $ >= 0是无法成立的，如果上面定义能通过，那就说明Whiley用的自动定理证明还不完善。而事实上，Whiley的int是任意长度的，完全避免了这个问题（可能有性能消耗）。

最后这变成个选择问题。要性能、数字不大就用和机器字对应的，必要的时候要自己检查。数字很大就牺牲点性能用不限长度的的。

2013-08-22: 才发现，其实用一个符号位加一个正整数就可以了～～