Side Effects in Steering Fragments

TL;DR

This thesis formalizes the concept of side effects in programming by extending Dynamic Logic to DLAf, allowing precise evaluation and classification of side effects in deterministic programs, including real systems like PGA.

Contribution

It introduces DLAf, a novel logic system that models side effects with short-circuit evaluation and provides a framework for analyzing and classifying side effects in programs.

Findings

Defined side effects as differences between actual and expected evaluations.

Developed rules for composing side effects in instructions.

Applied the system to real systems like Program Algebra (PGA).

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 DLAf (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 DLAf 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 \dlaf-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).