infinite-looppost-conditionshoare-logic

Hoare Logic | What post-condition is valid when there is an infinite loop?

My teacher told me the following statement is valid: {x > 3} while true (x := 3) {x = 3}

Why is this statement valid? Is it because the post-condition never gets checked, or will the post-condition now count as an invariant check?

In short: can the post-condition just be anything when there is an infinite loop?

Then this will be valid: {x > 3} while true (x := 3) {x = 0}

Solution

  • An infinite loop can have any postcondition at all (including something completely silly like 1=0) and it will be vacuously true. In fact, an always-false postcondition is a way of enforcing that a loop can never exit.