All 4 parts to this question concern the assertion P = {x=2^K & N>K}

and one of 4 different assignment statements. You are to supply the

missing assertions Q1, Q2, Q3, and Q4. Note that Q1 and Q2 should

be the weakest preconditions for P with respect to the given statement;

Q3 and Q4 should be postconditions with respect to the given statement

whose weakest precondition would be P.

Hint: The assignment axiom does not apply directly in the forward

direction as in (c) and in (d). However, you can guess at Q3 and Q4

by "looking" for x/4 and for K+1 in P and then substituting in reverse.

You should then check your answer; i.e., check whether your

post conditions do indeed have P as their weakest precondition using

the assignment axiom directly.

a)

{ } = Q1

y <-- y/N

{x=2^K & N>K}

(b)

{ } = Q2

x <-- x+x

{x=2^K & N>K}

(c)

{x=2^K & N>K}

x <-- x/4

{ } = Q3

}

(d)

{x=2^K & N>K}

y <-- K+1

{ } = Q4

a)Attempt

For this I see that

(y<-- y/N) means Any y is replaced by y/N

y/N is equivalent to N <--- y

so y <---- N <---- y

So the precondition is

Q1= {x=2^K & y>K}

well I not too sure about this.

I think it could be Q1= {x=2^K & N>K}

b)Attempt:

x <-- x+x means replace x with x+x

So Q2={ x+x =2^k & N>K}

I don't think this is the weakest precondition.

can this be simplified?

c)Attempt:

Q3={x/4=2^K & N>K}

Im not too sure...

d)Attempt:

Post Condition

Q4={x=2^(K+1-y+k)-y & N>K+1-y+K}

When I replace K+1 with Y

I get x=2^y-y+k & N>y-y+K

this is exactly the same as the precondition

Can someone check my answers and help me explain what the ones I get wrong?