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?


1 Answer 1


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

By soundness: |={x=43} x:=x+1 {x=44}


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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