Formalizing programming variables in process algebra
Jcm Jos Baeten, V. Bos · 2002
We use an existing ACP-style process algebra as a formal framework for imperative sequential programming. The framework is realized by instantiating this process algebra with a suitable set of atomic actions and providing concrete definitions for the auxiliary functions assumed by this process algebra. In this framework, we can reason algebraically about programs with assignments and programming variables. We show the programming variables obey scoping rules known from existing programming languages. Next, we use the framework to define well known constructs of sequential programming languages, like conditional statements and loops, and show laws characterizing these constructs can be proved using the ACP axioms.