Confusion about assignment axiom in Hoare logic

Question

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?

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}