Axiomatic semantics: Pre-post semantics of Graal

pp 319-322 Assignment
The axiom schema for assignment uses the notion of *substitution*.

This rule applies to languages which draw a clear distinction between
the notions of expression and instruction. In such languages,
expressions produce values, with no effect on the run-time state of
the program; in contrast, instructions may change the state, but do
not return a value. This separation is violated if an expression may
produce *side-effects*.

Functions which produce arbitrary side-effects are bad programming
practice, they are damaging referential transparency.

pp 335-336
The "Law of the excluded miracle" by Dijkstra states that no
instruction can ever produce the postcondition False:

	a wp False = False

[wp: weakest precondition]

a wp True is the weakest precondition that will ensure termination of
a.

p 337
For any assertion Q:

	Skip wp Q = Q
	Abort wp Q = False

What Abort "does" practically is irrelevant to the theory. To
paraphrase Wittgenstein's famous quote: What one cannot prove about,
one must not talk about.