Partial Correctness

A partial correctness statement in Hoare Logic or Separation Logic is a triple \Hoare ⁢ P ⁢ C ⁢ Q \Hoare 𝑃 𝐶 𝑄 \Hoare{P}{C}{Q} states that a program C 𝐶 C that starts in a state P 𝑃 P only terminates in states validating Q 𝑄 Q .

If we use Relational Semantics for our programming language, this boils down to ⟦ C ⟧ ∘ P ⊆ Q \llbracket{C}\rrbracket\circ P\subseteq Q , where the predicates P , Q 𝑃 𝑄 P,Q are viewed as relations ⊤ → S → Ω \top\to S\to\Omega .