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 yourpost conditions do indeed have P as their weakest precondition using the assignment axiom directly.
a)
{ } = Q1
y <-- y/N
{x=2^K & N>K}
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}
(b)
{ } = Q2
x <-- x+x
{x=2^K & N>K}
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)
{x=2^K & N>K}
x <-- x/4
{ } = Q3
Attempt:
Q3={x/4=2^K & N>K}
(d)
{x=2^K & N>K}
y <-- K+1
{ } = Q4
Attempt:
There are no y so I cant replace anything.
Q4={x=2^K & N>K}
I have lots of doubts about my answers.
Some help would be appreciated.