Math 2.0

Proposition

Empty statement axiom schema

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.

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

Further reading

  1. Wikipedia, page 182708, revision 1359292368, Hoare logic, section Rules > Empty statement axiom schema. adopted
About this page
Tag2H88557S7F
URIm2://2H88557S7F
Kindstatement, proposition
WritingW0 stub
StatusThis copy of the site has no build data. Run m2 status 2H88557S7F.
Changed4 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • edge uses out: each definition that the statement needs (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.