---
tag: 2H88557S7F
kind: statement
role: proposition
name: Empty statement axiom schema
sources:
  - wikipedia: en:182708@r1359292368
    locator: Hoare logic, section Rules > Empty statement axiom schema
    note: adopted
    mention: wikipedia://en/182708#MZU6
    sections: [Statement]
inventory: [KWQYJC4FWF]
---

## Statement

The empty statement rule asserts that the skip statement does not change the state of the program, thus whatever holds true before skip also holds true afterwards.

$$\dfrac{}{\{P\}\texttt{skip}\{P\}}$$