CODEWITHSUNDEEP
c++assertionspreconditions
erbisme4
erbisme4

Reputation: 31

c++ preconditions/assertions

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}.

Upvotes: 3

Views: 1808

Answers (5)

Jim Balter
Jim Balter

Reputation: 16406

If x > 0, y >= 0 is always satisfied due to if (x > 0) y = x. If x == 0, y >= 0 is always satisfied due to if ( x > 0) ... else y = -x. If x < 0, y = -x so y >= 0 is satisfied unless -x < 0. So the precondition is { x >= 0 || -x >= 0 }. (The only value of x for which that isn't true is the max neg value, which overflows.)

{ y >= 0 && |y| == |x| } is better than { y >= 0 } because the latter is true for all sorts of functions, not just one that finds the absolute value of x (which is presumably what this code is for, although you seem to have elided vital parts of the problem statement).

Upvotes: 0

Tony Delroy
Tony Delroy

Reputation: 106096

If you're doing this to learn about programming, you can do a bit of programming to help you confirm the answer:

#include <iostream>

int abs(int x) { return x >= 0 ? x : -x; }

int main()
{
    for (int i = -128; i <= 127; ++i)
    {
        char x = i;

        char y;

        if (x > 0)
            y = x;
        else
            y = -x;

        if (!(y >= 0 && abs(y) == abs(x)))
            std::cout << "failed for " << i << " (y " << (int)y << ")\n";
    }
}

Running this you'll see if fails for x -128 (where y is -128). This is due to the asymmetry in 2's complement notation: -128 can be represented in an 8-bit char, but 128 can not (only 127).

So for 1, and assuming 2's complement integers, the precondition is that x is not the lowest representable value in your bit width. Of course, there's nothing in the question that says x and y are even ints, so it's all a bit tentative.

If x and y were floats or doubles say, then in the normal IEEE representations there's a sign bit that can be toggled without affecting the mantissa or exponent, allowing a "clean" change of sign. That said, there are also corner cases with "not a number" (NaN) and (positive and minus) infinity sentinel values, which it would be wise to check either experimentally and/or by studying the representations and behavioural specifications....

Describe why [{ y >= 0 && |y| == |x| }] is better for verifying the code than just { y >= 0}.

A vague question, as we've no certainty about what the code's trying to achieve, and our reasoning about that comes circularly from the assertion that the former post-condition is better than the latter. Still, they're fishing for an answer like: the former also ensures the absolute magnitude of y survives whatever the sign change made by the code does to x.

In practice for our 2's complement integers the magnitude did always match afterwards - it was the sign part of the post-condition that flagged the corner case. But, it's still reassuring to have that extra insight into what's expected.

Upvotes: 2

amdn
amdn

Reputation: 11582

The answer to this can get messy depending on the type for x and y. As @PeteFordham pointed out integers in two's complement aren't symmetric, the absolute value of the maximum negative integer cannot be represented. If instead of integers x and y are float or double then you have to consider that in IEEE format zero can have both a positive and negative sign.

#include <iostream>
int main() {
    double x = 0;
    double y = -x;
    std::cout << "x=" << x << " y=" << y << std::endl;
}

the output is

x = 0 y = -0

Upvotes: 1

Pete Fordham
Pete Fordham

Reputation: 2343

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 }

Upvotes: 2

stark
stark

Reputation: 13189

Work backwards from the post condition. There is only one branch statement. Since the if statement tests x > 0 then just look at the 3 cases: x < 0, x == 0, and x > 0 to determine which values of x satisfy the post-condition.

Upvotes: 0

Related Questions