invariant P
invariant Q \/ P /\ R
invariant R
do X /\ Y → skip; abort
 ⫾ true   → while Z do skip od od