# Using the Consequence Rule

I have the following example that I have to prove

{a>7 ^ b>=0} n:=a-b {n<a ^ a+b>=0}


Using the Consequence Rule I assumed that the P is true

{true} n=a-b {n<a ^ a+b>=0}


so logically, the Q should be true, but I'm not sure if that'd be enough.

• I don't think "Consequence Rule I" is a standard notion. – Yuval Filmus Nov 19 '17 at 22:44

Here is what you need to prove:

If $a > 7$, $b \geq 0$ and $n = a-b$ then $n < a$ and $a+b \geq 0$.

By the way, this is actually false, since if $b = 0$ then $n = a$. Perhaps you miscopied?

• well not equal to a, but whatever the value of a-b gets assigned to n – A. muffin Nov 19 '17 at 22:52

To do this systematically, with the rules of Hoare logic, proceed as follows.

First, use the assignment axiom to generate a valid Hoare triple of the form $\{\phi\}n \mathbin{:=}a-b\{n<a \land a+b\geq 0\}$.

Then use the consequence rule to derive the Hoare triple you're after. Besides the Hoare triple we just found, this instance of the consequence rule will have a premise $a>7 \land b\geq 0 \Rightarrow \phi$. You need to prove that it is valid, too, but that's a maths task independent of Hoare logic. As Yuval observed in his informal explanation, you will fail to prove this.