0
$\begingroup$

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.

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

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?

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

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.

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