Hoare triple of non-terminating command?

[yookoon]

Definition hoare_triple (P:Assertion) (c:com) (Q:Assertion) : Prop := ∀st st', c / st ⇓ st' → P st → Q st'.

Above is the formal definition of hoare triple given in hoare.v

Then is the following hoare triple {{True}} WHILE True DO SKIP END {{False}} valid since there is no such state st' such that c / st ⇓ st' holds?

[jaewooklee93]

Yes, it is.

Theorem loop_exfalso:
  {{fun st => True}}
  WHILE BTrue DO SKIP END
  {{fun st' => False}}.
Proof.
  eapply hoare_consequence_post.
  - apply hoare_while.
    unfold hoare_triple; eauto.
  - intros st' [_ contra]; inversion contra.
Qed.

[yookoon]

Thanks!