UTP Semantics of Reactive Processes with Continuations

Abstract

Based on the Unifying Theories of Programming (UTP) semantic framework, Hoare and He have defined (a means for constructing) a high-level language with labels and jumps, using the concept of continuations. The language permits placing labels at given points within a program and making jumps to these labels when desired. In their work, Hoare and He have limited themselves to the definition of continuations for sequential programs. This paper is concerned with the extension of that work to reactive programs. We first extend their results to include parallelism and Higher Order programs. This is achieved by designing a new control variable $\mathcal {L}$ whose value follows the parallel structure of programs. We then proceed to define reactive (CSP) processes that contain the new control variable $\mathcal {L}$, resulting in the theory of Reactive (Process) Blocks. The encapsulation operator defined by Hoare and He and which may also be used for hiding the control variable $\mathcal {L}$ does readily provide a (functional) link between both UTP theories of Reactive Processes and of Reactive Blocks. The semantics are denotational.