Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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.
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?
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.
