What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic? Having learned a rough summary of Hoare logic (i.e. learning just the basic concept of Hoare triples and a few of the rules) I kept seeing a statement along these lines:


  The rule of consquence allows us to strengthen the precondition and weaken the postcondition. (paraphrased)



What does it actually mean to strengthen the precondition and to weaken the postcondition?
Is and used in its strict logical meaning in this sense, i.e. if we apply the rule of consequence we will always do both? Or can it be read as allowing us to choose to strengthen the precondition or weaken the postcondition?


I get the (very basic) idea of the rule, but this statement implies the rule can be applied for a strategic reason that isn't clearly explained.

Thanks.
Condition&nbsp;$A$ is stronger than condition&nbsp;$B$ if $A$ implies&nbsp;$B$.  That is, if $B$&nbsp;holds in all situations in which $A$&nbsp;holds.  Conversely, if $A$ is stronger than&nbsp;$B$, then $B$ is weaker than&nbsp;$A$. Note that, from the definition, $A$&nbsp;is stronger and weaker than itself, since $A$ implies&nbsp;$A$.  (We might prefer to say "at least as strong as" instead of "stronger than" but I guess that gets convoluted and it's easier to just remember that "stronger than" really means "at least as strong as".)

So, to strengthen a condition is to replace it with a stronger one; to weaken a condition is to replace it with a weaker on. Because a condition is always stronger and weaker than itself, the phrase "strengthen the precondition and weaken the postcondition" does indeed mean that we can leave one (or even both!) of them unchanged.