4
$\begingroup$

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.

$\endgroup$
8
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ @Dave I've not looked at Hoare logic since I was an undergrad so I'm afraid I don't have any examples to hand. $\endgroup$ – David Richerby Nov 3 '16 at 8:35
  • 2
    $\begingroup$ Quite often you try to prove that X implies Y and you can't - because X is actually too weak and Y too strong to make the statement true, or because you are not clever enough. You may try to strengthen the precondition X or weaken the postcondition Y to create a statement that is true / that you can prove. $\endgroup$ – gnasher729 Nov 3 '16 at 8:59
  • 2
    $\begingroup$ On the other hand, once you have proved that X implies Y, you would look how you can weaken the precondition X or strength the postcondition Y and still have a statement that is true or that you can prove. $\endgroup$ – gnasher729 Nov 3 '16 at 9:00
  • 1
    $\begingroup$ @gnasher729 That makes a lot of sense. I have a rudimentary exposure to proofs from reading on my own and I can see how that would apply now. That also lines up with induction vs strong induction as I understand it. So now I feel on a bit firmer ground with the concept. Thanks! $\endgroup$ – Dave Nov 3 '16 at 19:16
  • 1
    $\begingroup$ @DavidRicherby not a problem, thanks for taking the time to spell out what you did, it was still very helpful. $\endgroup$ – Dave Nov 3 '16 at 19:17
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.