Search

Algebraic operational semantics is further developed and used to provide meanings for Modula 2. A distinguishing feature of the approach is that it is geared towards resource sensitive programs which may use multi-processing. The semantic theory developed is operational. Each state of a computation is a static mathematical structure--a finite many-sorted first-order structure with partial functions. I.e., each state consists of a collection of finite sets, together with a number of relations and (possibly partial) functions. For Modula 2 the universes will include an interval of integers, a set of truth values, a set of characters, etc.--denotations for Modula data types--plus other finite sets such as a universe whose elements represent program variables, a universe of locations to represent incarnations of program variables, etc. The functions provide operations on the denotations of data types, assign locations to the representatives of program variables, assign values to locations, etc. A structure evolves from one state to another according to transition rules that depend only on the language for which the structure is tailored. Both universes and functions are allowed to change: universes may acquire or lose elements and functions may have their domains or ranges altered. The dynamic meaning of programs is modelled. Unlike previous operational semantics, the algebraic approach attempts to formalize directly a programmer's intuitive underst and ing of the operational meaning of programs. The abstraction level of our ideal machines is exactly that of the given programming language; the machines are tailored explicitly for the language. The ideal machines usually have bounded resources. All of a structure's universes are finite. Finite machines are not necessarily viewed as approximations to infinite ones. One goal is to provide both a pedagogical tool and a st and ard by which the correctness of implementations can be assessed. It is also a basis for applying the logic of dynamic structures. In addition, the theory is extended to certain low level facilities of a hypothetical implementation and then used to prove the correctness of a program that makes use of these facilities.