c++ preconditions/assertions

Question

This is not my homework -- I'm just practicing. I can't seem to wrap my mind around this assertion concept.

1) Determine the pre-condition for x that guarantees the post-condition about y
{ _______ }
if (x > 0)
    y = x;
else
    y = -x;

{ y >= 0 && |y| == |x| }
2) This code is the same as has been seen before, but the post-condition is different.                    
Describe why this post-condition is better for verifying the code than just { y >= 0}.

Answer 1

I'd guess because typically an integer type can represent from (-N) > 0 > (N-1). That is to say if your int is a signed 32 bit integer it could hold the value -2147483648 but not the value 2147483648.

{ x != INT_MIN }