プログラムの実行前後に成り立つ命題を表す、公理的意味論の記法。

$$\{P\}\;C\;\{Q\}$$

• $P$：実行前に成り立つ 事前条件
• $C$：実行するプログラム
• $Q$：実行後に成り立つ 事後条件

通常の部分正当性では、「$P$ が成り立つ状態から $C$ を実行し、$C$ が停止したなら、実行後には $Q$ が成り立つ」と読む。

どのホーアトリプルを導けるかは、ホーア論理の公理と推論規則によって定める。