Editing Hoare logic (section)

===Empty statement axiom schema===

The [[NOP (code)|empty statement]] rule asserts that the {{mono|skip}} statement does not change the state of the program, thus whatever holds true before {{mono|skip}} also holds true afterwards.<ref group=note>This article uses a [[natural deduction]] style notation for rules. For example, <math>\dfrac{\alpha,\beta}{\phi}</math> informally means "If both {{mvar|&alpha;}} and {{mvar|&beta;}} hold, then also {{mvar|&phi;}} holds"; {{mvar|&alpha;}} and {{mvar|&beta;}} are called antecedents of the rule, {{mvar|&phi;}} is called its succedent. A rule without antecedents is called an axiom, and written as <math>\dfrac{}{\quad\phi\quad}</math>.</ref>

: <math>\dfrac{}{\{P\}\texttt{skip}\{P\}}</math>