 Vacuous truth

A logical implication holds whenever its premise is false. For partial correctness, an execution that never terminates supplies no final state violating the postcondition.