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 definition. 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.
http://i.stanford.edu/pub/cstr/reports/csl/tr/78/155/CSL-TR-78-155.pdf