Finding the Weakest Precondition (Hoare Logic)

[Shinichi72]

Here is the problem, I have tried to compute it and provide a solution. But, my teacher told me that it is wrong. Maybe the final answer is not simplified or there is a miscomputation in my solution.

Consider the following expression: x = 2 * y + x - 1 {x > 11}

Applying the assignment axiom we have the weakest precondition to be

{2 * y + x - 1 > 11}

{2 * y + x > 12}

{2 * y > 12 - x}

{y > 6 - (x/2)}

The weakest precondition is {y > 6 – (x/2)}.(My answer is not correct)

For a better understanding, I will provide a meaning of finding the weakest precondition and an example that will definitely help you to understand my problem.

An axiom for assignment statements x =: E
{P} x =: E {Q}
➔
Given an assignment statement x =: E and a
postcondition Q, we can compute its weakest
precondition P by using Q with all instances of x
replaced by E, denoted by the assignment axiom
P = Q x → E

Example
{???} x =: x + y - 3 {x > 10}
➔Even if the LHS of the assignment (i e x appears in the
RHS does not affect the process of computing the precondition, as in

x + y - 3 > 10
y > 13 - x
∴{y > 13 x} x =: x + y - 3 {x > 10} is correct

 

[Dr.Peterson]

For those who don't know, this is a repost of https://www.freemathhelp.com/forum/threads/finding-the-precondition.129104/

Example
{???} x =: x + y - 3 {x > 10}
➔Even if the LHS of the assignment (i e x appears in the
RHS does not affect the process of computing the precondition, as in

x + y - 3 > 10
y > 13 - x
∴{y > 13 - x} x =: x + y - 3 {x > 10} is correct

Unfortunately, the example shows no reason to think your answer of {y > 6 – (x/2)} would not be correct.

When your teacher says it is not correct, do you mean you submitted this as an answer to your teacher, and all he said was that it is not correct, with no helpful information about why? Or is it a computer that tells you the answer is wrong? Or are you told something more? I am looking for any clue at all. And are you not allowed to ask your teacher what is wrong, so you can correct it? That is what I meant by asking your teacher to teach!

I don't think you have yet given a direct quotation of the problem as given to you. There may be some fact you have omitted (e.g., if x and y are integers) that would change our answer. From everything I've read, even an unsimplified answer should be called correct, and what you have done seems to be appropriate simplification.

 

[Shinichi72]

For those who don't know, this is a repost of https://www.freemathhelp.com/forum/threads/finding-the-precondition.129104/


Unfortunately, the example shows no reason to think your answer of {y > 6 – (x/2)} would not be correct.

When your teacher says it is not correct, do you mean you submitted this as an answer to your teacher, and all he said was that it is not correct, with no helpful information about why? Or is it a computer that tells you the answer is wrong? Or are you told something more? I am looking for any clue at all. And are you not allowed to ask your teacher what is wrong, so you can correct it? That is what I meant by asking your teacher to teach!

I don't think you have yet given a direct quotation of the problem as given to you. There may be some fact you have omitted (e.g., if x and y are integers) that would change our answer. From everything I've read, even an unsimplified answer should be called correct, and what you have done seems to be appropriate simplification.

The computer tells my answer that it is wrong, but I have concluded that the answer that I have submitted on the computer (because we have an online learning platform) have already seen by my teacher, that is why I have told you that my teacher told me that my answer is wrong. By the way, we have unlimited attempts to submit our answer, I already have tried many answers such as y> 6-x/2, y> -(x/2)+6, y>6-x, and y>-x+6 with our without spaces, but it always gives me an X(wrong) mark.

But if you found no reason that my answer of {y > 6 – (x/2)} would not be correct. Then, I will just tell my teacher and explain my point. And thank you for your efforts to help me.

 

[Dr.Peterson]

I'd love to see an image of the problem and what it shows for your answer. And if you find out from your teacher, please tell us and relieve the mystery.

I myself would have tried {x > 12 - 2y}.

 

[Shinichi72]

I'd love to see an image of the problem and what it shows for your answer. And if you find out from your teacher, please tell us and relieve the mystery.

I myself would have tried {x > 12 - 2y}.

Good Day, Dr. Patterson, I'm really glad for your help. By the way, I took your advice for trying your answer which is {x > 12 - 2y} but I just made a few changes and here is my answer y>(12-x)/2, which is actually correct now.

 

[Dr.Peterson]

I hope you eventually find what the requirement is for a "correct" answer. Clearly what it accepted is algebraically equivalent to your original answer.

It's conceivable that the question was just programmed wrong, so that it doesn't recognize equivalent answers, and most of the answers that have been rejected are really correct.