0
$\begingroup$

I wanted to know if we are given the f.f.g. Hoare triple:

{x = 43}x := x + 1{x = 44}

How do we show that this is a valid Hoare triple?

My attempt was:

Using the assignment axiom: {x + 1 = 43} x := x + 1 {x = 44}

But this doesn'the make sense. I also want to know what went wrong in my attempt?

$\endgroup$
2
$\begingroup$

The assignment axiom in standard Hoare logic says:

|- {P[e/x]}x:=e{P}

If you choose P[e/x] to be x+1=44 (that is e is x+1) you get:

|- {x+1=44} x:=x+1 {x=44}

By the consequence rule, since: |= x=43 --> x+1=44, and |= x+1=44 --> x+1=44, and
|- {x+1=44} x:=x+1 {x=44}

you know that |- {x=43} x:=x+1 {x=44} .

Since the Hoare logic is relatively complete you know that: |={x=43} x:=x+1 {x=44}

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