A formal semantics for imperative compensations

Abstract

Formal Semantics deal with the study of meaning of a programming language. A formal specification is a way to describe a programming language precisely and unambiguously. At the moment, a lot of work was done on formalising compensations. A compensation is an action that is associated with another action. When the compensation is executed, it cancels the effects of the activity it is associated with. Programming languages and libraries based on compensations are usually specified informally. 'I'he language behaviour is described using natural languages which tend to be ambiguous. The only interpretation of the language is what the compiler outputs. The aim of this FYP is to develop an operational semantics for an imperative programming language that uses compensations as part of its error recovery mechanism. At the moment only a written documentation is available for the said language. We will create a set of reduction rules that describe the behaviour of the language constructs. The proposed semantics could then be used as a precise and unambiguous standard for the language.