An Axiom
Syntax/Notation:
{ P } S { R }
P is precondition
S is program
R is
post-condition
Semantics:
If P is true before S starts,
and if S successfully terminates
R will be true after S terminates.
S is proved to be
conditionally
correct, i.e.,
If S terminates, it is correct.