Posted on October 4, 2022 Semantics of {P}c{Q}: Hoare logic: P s, s–(c)→s' => Q s' Separation logic: P s, safe c s ∧ s–(c)→s' ⇒ Q s'