Report Number: CSL-TR-78-155
Institution: Stanford University, Computer Systems Laboratory
Title: The formal definition of a real-time language
Author: Hennessy, John L.
Author: Kieburtz, Richard B.
Date: July 1978
Abstract: This paper presents the formal definition of TOMAL
(Task-Oriented Microprocessor Application Language), a
programming language intended for real-time systems running
on small processors. The formal definition addresses all
aspects of the language. Because some modes of semantic
definition seem particularly well-suited to certain aspects
of a language, and not as suitable for others, the formal
definition employs several, complementary modes of
The primary definition is axiomatic in the notation of Hoare;
it is employed to define most of the transformations of data
control states affected by statements of the language.
Simple, denotational (but not lattice-theoretic) semantics
complement the axiomatic semantics to define type-related
features, such as the finding of names to types, data type
coercions, and the evaluation of expressions. Together, the
axiomatic and denotational semantics define all the features
of the sequential language.
An operational definition, not included in the paper, is used
to define real-time execution, and to extend the axiomatic
definition to account for all aspects of concurrent
execution. Semantic constraints, sufficient to guarantee
conformity of a program with the axiomatic definition, can be
checked by analysis of a TOMAL program at compilation.