What does it mean to "strengthen the precondition and weaken the postcondition" in Hoare logic?

Question

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)

1. What does it actually mean to strengthen the precondition and to weaken the postcondition?

2. 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.

Answer 1

Condition $A$ is stronger than condition $B$ if $A$ implies $B$. That is, if $B$ holds in all situations in which $A$ holds. Conversely, if $A$ is stronger than $B$, then $B$ is weaker than $A$. Note that, from the definition, $A$ is stronger and weaker than itself, since $A$ implies $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 "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 one. 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.

Answer 2

The consequence rule is a necessary${}^*$ piece of glue we typically apply in a few select situations around loops.

1. We're trying to prove $\{\psi\}\mathbf{while}~g~\mathbf{do}~P~\mathbf{od}\{\phi\}$ but the standard rule $$\frac{\{I\land g\}P\{I\}}{\{I\}\mathbf{while}~g~\mathbf{do}~P~\mathbf{od}\{I\land\neg g\}}$$ where $I$ is our loop invariant doesn't quite fit because the $\psi$ and $\phi$ typically don't mention local variables such as counters used to control the loop. But those are crucial to express $I$. So we use the consequence rule, having to show $\psi\Rightarrow I$ and $I\land\neg g\Rightarrow\phi$ to link up with the outside.
2. When proving the hypothesis of the rule above, we work our way up backwards through the body $P$ of the while loop, from the invariant $I$ which we want to hold again at the end of the body all the way to the beginning of the body, where we arrive at an assertion $K$. But we know already what assertion we want to hold there: $I\land g$. Typically the two assertions are not the same but if we have a good invariant, then we'd at least be in a position to prove the implication $I\land g\Rightarrow K$, which allows us to use the consequence rule once again as glue.
3. Initialisation code such as $x := 0; i := n$ is usually present to remove the dependence on a precondition such as $x=0\land i=n$, yet, Hoare logic without consequence rule only gives us $0=0\land n=n$ as precondition $\psi$ in $\{\psi\}x := 0; i := n\{x=0\land i=n\}$. Yes, I agree that this isn't exciting but technically we need to bridge the purely syntactic gap between the intended precondition $\mathit{True}$ and the semantically equivalent $0=0\land n=n$. Note that in the previous two cases we had bridge semantic gaps.

${}^*$ This is a mathematical "necessary" in the sense that Hoare logic without the consequence rule fails to prove many semantically valid Hoare triples the Hoare logic with it manages to prove.