Given the following loop:

while x> 0

sum = sum + x;

x = x - 1;

end loop

For each of the following conditions: 1) x is in the set of {counting numbers} 2) x is in the set of {Whole numbers} 3) x is in the set of {integers}

Define the appropriate postcondition for x. Define the associated loop invariant and the weakest precondition for the loop. Prove your answer is correct using the 4 necessart conditions for pretest loops.