Handling expressions with side effects within an axiomatic semantics framework

This paper shows how expressions with side effects can be treated in an axiomatic framework. The first problem is defining an appropriate valuation function. This is done by defining evaluation orders and showing how this can be used to define appropriate valuation functions. A syntactic transformation that eliminates all expressions with side effects is then presented. This transformation yields a program that is equivalent to the original program but has no expressions with side effects. This new program can be then handled with the standard axioms.<>