severity 430126 wishlist
thanks
Hi,
Jiří Paleček wrote:
> the "abs" example, which is bundled with caduceus, is not really correct.
>
> What's the problem:
>
> /* @ensures \result > 0 */
> int abs(int x) { return x<0 ? -x : x; }
>
> This number work for all integers, except for one. In the base-2
> complement,
> there are two numbers which staisfy x==-x. One is 0, and the other is
> 0x80000000 hex (on 32 bit architecture), which is negative. therefore,
> abs(this number) is negative.
Why only supports mathematical integers for now. Modular integers are
supported in the cvs version of why and will eventually make their way
into the released version of why.
Cheers,
Samuel.
