A semantics for while with break, continue and goto

Abstract

This work presents a formal description of a subset of a C-likelanguage in the form of an operational semantics. We give semantics to the following statements (presented in alphabetical order) : assig- nation, break, composition, continue, goto, if, skip and while. The semantics is given by an abstract machine composed by an stack, two counters and three functions. We prove some expected properties of the semantics.