# Math Logic Finding the Weakest Precondition Calculus?

• Feb 17th 2010, 07:26 AM
jjbrian
Math Logic Finding the Weakest Precondition Calculus?

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.
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}
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?
• Feb 17th 2010, 08:26 AM
Plato
The questions you posted appear very course/textbook/instructor specific.
That is to say, unless some person is in that same class I doubt the person would any idea what is being asked.
• Feb 21st 2010, 01:15 PM
emakarov
This concerns Hoare Logic, a pretty standard way of reasoning about imperative programs.

Quote:

a)
{ } = Q1
y <-- y/N
{x=2^K & N>K}...

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}
I think it could be Q1= {x=2^K & N>K}
The general inference rule (axiom) is {P[t/x]} x <-- t {P} where P[t/x] denotes replacing x by t in P. Since y does not occur in the postcondition, Q1 is the same as the postcondition, i.e., x=2^K & N>K. Indeed, if this holds before the assignment, then whatever you assign to y, the same formula will still be true.

Quote:

(b)
{ } = Q2
x <-- x+x
{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?
You are correct, Q2 is (x=2^K & N>K)[x + x/x] (recall that [...] denotes a substitution), which is x+x =2^k & N>K. You can simplify it as 2x =2^k & N>K or x =2^{k-1} & N>K; this is not essential.

Quote:

(c)
{x=2^K & N>K}
x <-- x/4
{ } = Q3
Finding the postcondition is trickier than applying a substitution; one has to "un-apply" a substitution, so that Q3[(x/4) / x] is x=2^K & N>K. Well, 4x=2^K & N>K as Q3 seems to work.

Quote:

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
To check, you need to replace y with K + 1 in the postcondition, not the other way around. Here, since y does not occur in the precondition, Q4 is the same as that precondition.