We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.
To save content items to your account,
please confirm that you agree to abide by our usage policies.
If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account.
Find out more about saving content to .
To save content items to your Kindle, first ensure [email protected]
is added to your Approved Personal Document E-mail List under your Personal Document Settings
on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part
of your Kindle email address below.
Find out more about saving to your Kindle.
Note you can select to save to either the @free.kindle.com or @kindle.com variations.
‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi.
‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.
Task declarations initiate concurrent processes, which can synchronize using entry calls and accept statements. The select statement may now iterate until an entry call can be accepted.
The semantics of task declarations illustrates the use of the communicative action notation introduced in Chapter 10.
Semantic entities now include agents, and various signals sent in messages. They also include entities that represent open alternatives of selections.
Let us first consider the treatment of input and output in programming languages. By definition, the input of a program is the information that is supplied to it by the user; the output is the information that the user gets back. However, it is important to take into account not only what information is supplied, but also when the supply takes place. We may distinguish between so-called batch and interactive input-output.
With batch input, all the input to the program is supplied at the start of the program. The input may then be regarded as stored, in a file. Batch output is likewise accumulated in a file, and only given to the user when (if ever) the program terminates. On the other hand, interactive input is provided gradually, as a stream of data, while the program is running; the program may have to wait for further input data to be provided before it can proceed. Similarly, interactive output is provided to the user while the program is running, as soon as it has been determined.
Action notation includes a data notation for general use.
Standard data consists of tuples, truth-values, numbers, characters, strings, lists, trees, sets, and maps.
Some of the operations of data notation are intended for use mainly on proper sorts, rather than on mere individuals.
Appendix E gives the full algebraic specification of data notation.
Consider an implementation of a high-level programming language. When a program is run, the information processed by it is represented entirely by sequences of bits: O's and 1's. The programmer, however, does not usually have to deal with this representation directly. The program can be regarded as processing abstract entities, such as numbers, arrays, and sets. Indeed, standards for high-level programming languages generally leave the binary representation of information unspecified. Recall from Chapter 1 that the semantics of a program is an entity which represents the implementation-independent aspects of its information processing behaviour, and that the semantics of a phrase is an entity which represents its contribution to overall behaviour. In action semantics, these entities are generally actions. The information processed by programs is represented by items of data, which correspond directly to abstract entities such as numbers rather than to bit sequences.
Various sorts of data are needed for the semantics of general-purpose high-level programming languages, not only ‘mathematical’ values such as numbers and lists, but also abstract entities of computational origins such as variables, procedures, packages, and so on.
Action notation includes a declarative action notation for specifying scopes of bindings.
Declarative actions are concerned with scoped information.
Chapter H illustrates the use of declarative action notation in the semantic description of declarations, expressions, and statements.
Declarative actions axe concerned with processing scoped information, which generally gets propagated further than transient information. The scoped information current at the start of an action is often current throughout the action—although it may get temporarily hidden by other scoped information within the action. It disappears at the end of its scope.
Scoped information represents the associations, called bindings, which declarations in programs establish between identifiers and entities such as constants, variables, procedures, etc. Implementations usually represent bindings by some form of symbol table.
Programming languages are often characterized as having static or dynamic scopes for bindings. The difference concerns whether or not it is possible to determine from the program text, before running the program with its input, which declarations establish the bindings of which identifiers. For efficiency, compilers extract the required information from the symbol table during compilation, so that it isn't needed when the compiled code is run.
The possibility of dynamic bindings only arises when the programming language contains procedures, or similar constructs, where the body of the procedure can be called from various parts of the program: the bindings current at each call might be different.
Subprograms are classified as procedures or functions.
Procedures are parameterized statements. They may be declared, and then called with various actual parameters. Formal parameter declarations resemble incomplete constant and variable declarations.
Functions are essentially parameterized expressions.
The semantics of subprogram declarations and calls illustrates the use of the reflective action notation introduced in Chapter 9, as well as the declarative action notation introduced in Chapter 7.
Semantic entities now include subprogram entities, which are formed from abstractions, and data that are used to distinguish subprogram returns from other reasons for abnormal termination of statement execution.
A procedure is a construct that incorporates a statement, which is known as the body of the procedure. A procedure declaration binds an identifier to a procedure. A procedure call statement causes the body of the identified procedure to be executed. In a few languages, procedures are provided as expressions; then a procedure declaration may be written just like an ordinary constant declaration.
A function is like a procedure, but a function body is essentially an expression, rather than a statement: it has to return a result. A function call is a kind of expression. In practice, most conventional programming languages allow impure functions, where the body is a mixture of statements and an expression.
The systematic informal description of action notation summarizes Part II, and gives further details. It is intended for reference
To make it self-contained, it starts by repeating most of the introduction to the concepts of actions, data, and yielders given in Section 1.5.2.
The symbols of action notation are explained below in the same order as they are introduced in Part II and Appendix B, as indicated below. See the start of Appendix B for a more detailed overview of the modular structure of action notation.
The algebraic specification of data notation given here is definitive. See Chapter 5 for an informal introduction to the various symbols. The occasional informal comment is inserted in the formal specification where appropriate.
The specification is divided into nested modules. The order of presentation of the modules is such that earlier modules do not often refer to later ones. In fact the submodules could be presented in a strictly bottom-up manner, but this would make navigation more difficult.
Reference to the module Data Notation/General includes all the specified modules except for the submodule Characters/ASCII, thus allowing specialization to alternative character sets. It also omits the Instant submodules, which are intended for use with the symbols translated to some specified sort.
Part III gives a progressive series of examples of action semantic descriptions. The programming constructs described all come from ADA. (NO previous familiarity with ADA is required, as the necessary concepts are all explained here.) The examples not only describe a substantial sublanguage of ADA, they also serve as paradigms for description of other programming languages. The description of constructs in the earlier examples remains unchanged in the later examples. This is in marked contrast to denotational semantics, where tedious reformulations of the earlier descriptions would be required when giving the later ones! Appendix A collects the examples together, for convenience of reference—and to show how a medium-scale action semantic description looks in its entirety. It also specifies the detailed specifications of semantic entities that are omitted in Part III.
Navigation
If this is your first reading, proceed in parallel through Parts II and III: Chapter 4, Chapter 11, Chapter 5, Chapter 12, and so on. This way, you see an illustration of the use of each part of action notation immediately after its introduction.
If you are already familiar with high-level programming languages, you could alternatively look at each chapter of Part III before the corresponding chapter of Part II. This way, the illustrations in Part III motivate the action notation introduced in Part II.
If you are revising, and would like an uninterrupted presentation of examples of action semantic descriptions, proceed straight through Part III.
The founding paper [Pratt 1976] on dynamic logic begins as follows:
“This paper deals with logics of programs. The objective is to formalize a notion of program description and to give both plausible (semantic) and effective (syntactic) criteria for the notion of truth of a description. A novel feature of this treatment is the development of the mathematics underlying Floyd-Hoare axiom systems independently of such systems.”
This book continues study of such mathematics with particular emphasis on semantic frameworks. We intend for these frameworks to be flexible, relying on no particular concept of state. Ultimately, extensions of the theory are to address at least program semantics, operating systems, concurrent processes and distributed networks; but the accomplishments of the foundational core herein are modest.
We shall be concerned with a category-theoretic foundation. One possible paradigm is that a morphism is the behaviour of a program. Composition of morphisms models program-chaining. An implementation of a programming language must provide a definite category in which to assign morphisms to programs. We shall also require that high-level specifications about programs map, as well, to true-false assertions about the corresponding interpreted programs.
Our semantic frameworks are categories satisfying certain axioms, that is, are models of the first-order theory of categories. Composition is the only primitive operation. Such models are strongly typed in that two morphisms cannot be composed unless the target of the first coincides exactly with the source of the second.
The original motivation for the development of action semantics was dissatisfaction with pragmatic aspects of denotational semantics.
Early work on abstract semantic algebras focused on the use of algebraic axioms to specify the intended interpretation of action notation.
Although the concrete form of action notation has varied greatly, the underlying primitives and combinators have remained rather stable.
The adoption of a meta-notation based on unified algebras simplified the algebraic specification of generic abstract data types, and allowed the use of operations on sorts in actions.
The provision of a structural operational semantics for action notation emphasized the operational essence of action notation, and allowed the verification of algebraic laws.
Recent enhancements of action semantics concern the grammars for specifying abstract syntax, action notation for communication and indirect bindings, and the notation for sorts of actions.
Current and future projects involve: the action semantic description of various programming languages; the implementation of systems supporting the creation, editing, checking, and interpretation of descriptions; action semantics directed compiler generation; and the further investigation of the theory of action notation.
The author welcomes comments on action semantics, and maintains a mailing list.
This concluding chapter explains the original motivation for the development of action semantics. It then gives what amounts to an annotated bibliography for action semantics and for its precursor, a framework called abstract semantic algebras. Finally, it describes current work, and invites you to participate in the future development of action semantics.