Side Effects in Steering Fragments
Lars Wortel

Abstract:
In this thesis I will give a formal definition of side effects. I will
do so by modifying a system for modelling program instructions and
program states, Quantified Dynamic Logic, to a system called DLA_f
(for Dynamic Logic with Assignments as Formulas), which in contrast to
QDL allows assignments in formulas and makes use of short-circuit
evaluation. I will show the underlying logic in those formulas to be a
variant of short-circuit logic called repetition- proof short-circuit
logic.

Using DLA_f I will define the actual and the expected evaluation of a
single instruction. The side effects are then defined to be the
difference between the two. I will give rules for composing those side
effects in single instructions, thus scaling up our definition of side
effects to a definition of side effects in deterministic DLA_f
-programs. Using this definition I will give a classification of side
effects, introducing as most important class that of marginal side
effects.  Finally, I will show how to use our system for calculating
the side effects in a real system such as Program Algebra (PGA).