ホーア論理
空文(skip文)は、プログラムの状態を変化させないが、これを表すのが空文の公理である。skip以前に真であったことはそのまま真となる。
{ P } skip { P }