JUCS - Journal of Universal Computer Science 10(9): 1272-1293, doi: 10.3217/jucs-010-09-1272
A Formal Model of Forth Control Words in the Pi-Calculus
expand article infoJames F. Power‡, David Sinclair§
‡ National University of Ireland, Maynooth, Ireland§ Dublin City University, Dublin, Ireland

Corresponding author: James Power ( jpower@cs.may.ie )

© James Power, David Sinclair.
This article is freely available under the J.UCS Open Content License.
Citation: Power JF, Sinclair D (2004) A Formal Model of Forth Control Words in the Pi-Calculus. JUCS - Journal of Universal Computer Science 10(9): 1272-1293. https://doi.org/10.3217/jucs-010-09-1272
Open Access
Abstract
In this paper we develop a formal specification of aspects of the Forth programming language. We describe the operation of the Forth compiler as it translates XSForth control words, dealing in particular with the interpretation of immediate words during compilation. Our goal here is to provide a basis for the study of safety properties of embedded systems, many of which are constructed using Forth or Forth-like languages. To this end we construct a model of the Forth compiler in the -calculus, and have simulated its execution by animating this model using the Pict programming language.
Keywords
Forth, picalculus, operational semantics