I have a question about determining preconditions for Hoare's Axiom Scheme. For example, if we have P { x=2 } x==1 and we are trying to determine the precondition, P, could we just set P as false giving us False { x=2 } x==1. I've read some of the other posts on this forum about Hoare's Axiom Scheme but am having a hard time wrapping my head around the topic.
$\begingroup$
$\endgroup$
1
-
$\begingroup$ It is not clear what you don't understand or disagree with. $\{\text{false}\}\, x:= 2\, \{x=1\}$ and $\{\text{true}\}\, x:= 2 \,\{x=2\}$ are two correct annotations. What is your question ? $\endgroup$– user16034Dec 12, 2022 at 13:49
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
Yes. You can set P to be false. However, the resulting statement won't be very useful.
Let's back up, and consider how to interpret a statement like P {x=2} x==2. This is saying that for every state of the program that satisfies P, if you execute x=2 in that state, then the state of the program afterwards will satisfy x==2. How useful is this? Well, the more states that satisfy, the more powerful and useful a statement this is -- the more you have learned.
So, a statement like true {x=2} x==2 is correct, and also very useful: it works no matter what the prior program state. It says that, no matter the previous program state, if you execute x=2, then the expression x==2 will hold afterwards.
In contrast, a statement like false {x=2} x==2 is correct, but not useful. It is correct, because it claims that for every program state that satisfies false, then executing x=2 will leave you in a program state where x==2. This is vacuously true, since there are no program states that satisfy false. However, it is not very useful. There are no program states that satisfy false, so there are no program states where this tells you something useful about what will happen if you execute x=2.
Now let's move on to the example you gave, of P {x=2} x==1.
How about true {x=2} x==1? This is incorrect. It's not true. If you start in a program state where, for instance, x==7, then this will satisfy true, but after executing x=2, the condition x==1 will not be satisfied. So, that's just a faulty claim.
How about false {x=2} x==1? This is a correct claim. For the same reasons as explained above, it is vacuously true. However, for the same reasons as explained above, it is not useful: there are no situations where this is a useful claim to know, since there are no program states that satisfy false.
Generally we look for the weakest precondition. Here a precondition that is "strong" is one that is restrictive; thus "False" is strong and "True" is weak. Notice that weak preconditions are one that apply to more prior states, and thus are more useful (can be applied to a larger set of prior states), so the weaker the precondition P, the more useful the statement will be. In other words, the weakest precondition is in some sense the most useful precondition. "False" is a very strong precondition; while it might be a valid precondition, it is not useful.
-
$\begingroup$ What do you mean "not useful" ? It does prove that the algorithm is not correct. $\endgroup$– user16034Dec 12, 2022 at 13:45
-
$\begingroup$ @YvesDaoust, Thanks for the feedback! I've revised my answer to try to elaborate on my reasoning. $\endgroup$– D.W. ♦Dec 13, 2022 at 4:51