• The abstract syntax of a kernel action notation is the basis for its formal semantic description. The full action notation can be reduced to the kernel by using some of the algebraic properties specified in Appendix B.

• The specification of semantic entities shows what kind of states are needed to support action performance.

• The structural operational semantics of action notation gives the formal definition of action performance.

• The definition of observational and testing equivalence on actions relates the operational semantics of action notation to the algebraic properties specified in Appendix B.

The standard action notation used in action semantics allows direct expression of control, dataflow, scopes of bindings, changes to storage, and communication between distributed agents. It is therefore to be expected that this Appendix, which contains its complete operational semantic description, makes a formidable document. The modular structure is shown on the next page. The modules are followed by the definition of observational and testing equivalence.

Whereas standard action notation is semantically rich, the kernel of action notation is syntactically of only moderate size. This is revealed by the grammar specifying the abstract syntax of the kernel. There are eight fundamental binary combinators, and four hybrid combinators. Disregarding the unfolding notation used to abbreviate infinite action terms, there are only two unary combinators in the kernel.

The metatheory so far has emphasized formulas. The more general first-order theory of Boolean categories must consider statements about both morphisms and formulas together. In this section we consider the equational theory of if-then-else in the “3-valued case” in which the corresponding choice operator is deterministic but not necessarily idempotent as was previously true in Proposition 5.13. Since “if P then α else α = α” is essentially the law of the excluded middle for P, we are therefore allowing such a law to fail, that is, “tests need not halt”. This is realistic in any context in which a test can query the result of an arbitrary computable function.

After characterizing 3-valued if-then-else in Boolean categories we pave the way for the main result, Theorem 14.9 below, as succinctly as possible. The proofs, which are of a universal-algebraic nature, are in [Manes, 1992]; the gap to be bridged in this section is to elevate the results of that paper to the setting of preadditive Boolean categories with projection system. At this time, however, the main result applies only to the semilattice-assertional case.

DEFINITION Let B be a Boolean algebra. The elements of B are “2-valued propositions”. A 3-valued proposition on B is a pair P = (PF, PT) with PF, PT ∈ B, PFPT = 0.

• Literals are lexical symbols including numerals, characters, and strings.

• The semantic description of literals is facilitated by standard operations on strings.

• The semantic entities required are specified ad hoc, exploiting the general data notation introduced in Chapter 5.

Literals are the simplest constructs of programming languages, with regard to both syntax and semantics. Typical examples are numeric literals, i.e., numerals, and string literals.

The description of literals is not very challenging. But we have to take care to avoid overspecification that might place unintended and impractical burdens on implementations.

For instance, it might be imagined that we could adapt the description of binary numerals in Chapter 2 immediately to decimal integer numerals, such as those in ADA. However, in the absence of syntactic limits on the length of numerals, the corresponding semantic entities would be arbitrarily-large numbers. Practical programming languages generally put implementation-dependent bounds on the magnitude of numbers. In ADA, the constants MIN_INT and MAX_INT bound the required integers, although implementations are allowed to provide further integer ‘types’ with implementation-dependent bounds.

The semantics of an integer numeral is the expected mathematical value only when that lies within bounds. Otherwise it should be some entity that represents a numeric error. The situation with literals for so-called ‘real’ numbers is similar, although it is necessary to take account of implementation-dependent lower bounds on the accuracy of ‘real’ numbers, as well as bounds on their magnitude.

• Algebraic specifications are used here for specifying standard notation for data, and for extending and specializing our standard notation for actions.

• Our unorthodox framework for algebraic specification copes well with partial operations, generic data, polymorphism, and nondeterminism.

• Algebraic specifications introduce symbols, assert axioms, and constrain models, as illustrated here by a natural example.

• The grammars and semantic equations used in action semantic descriptions can easily be regarded as algebraic specifications.

• The structural operational semantics of action notation is written as an algebraic specification of a transition function.

This chapter is mainly concerned with the details of how we specify notation for data. It also introduces the foundations of action semantics. Some readers may prefer to defer the detailed study of the example given here, because when reading action semantic descriptions one may take it for granted that data can indeed be specified algebraically, and that foundations do exist. Moreover, action notation does not depend much on the unorthodox features of our algebraic specification framework. On the other hand, readers who are used to conventional algebraic specifications are advised to look closely at this chapter before proceeding, as they may otherwise find it difficult to reconcile our examples with their experience.

First, some standard terminology. An algebra consists essentially of a universe, or carrier, of values, together with some distinguished operations on values. Operations of no arguments are called constants.

Part III initiates the study of a few issues concerned with the first-order theory of Boolean categories. “Formulas” are summands expressible in the language PBC of Boolean categories introduced in Section 11. The fundamental completeness theorem 11.15 asserts that a formula is universally valid if and only if it is true in the classical example of Mfn. A similar result holds for ranged Boolean categories. Using a completion by ideals developed in Section 13, the forward predicate transformers are seen to be categorically dual to the inverse ones, at least in the preadditive case. Section 14 provides the equational theory for 3-valued if-then-else in a Boolean category.

• Action notation includes an imperative action notation for specifying changes to storage.

• Imperative actions are concerned with stable information.

• Chapter 15 illustrates the use of imperative action notation in the semantic description of variable declarations, assignment statements, and expressions.

Imperative actions are concerned with processing stable information, which generally gets propagated further than transient and scoped information, remaining current until some primitive action changes it. Stable information consists of a collection of independent items, and each change only affects one item. Changes are destructive, rather than temporary, so they can only be reversed if a copy of the destroyed item is available.

Stable information represents the values assigned to variables in programs. An assignment is regarded as an order to the computer, rather than as an assertion, hence the adjective ‘imperative’ for the processing of stable information.

Implementations represent stable information using random-access memory, or secondary storage devices such as magnetic tapes and discs, which in fact can only store single bits—but lots of them! Particular bit-patterns in memory correspond to values, although different occurrences of the same bit-pattern may represent many different abstract values, such as characters and numbers. However, the representation of values by bit-patterns is generally implementation-dependent, so we are justified in ignoring it in semantic descriptions.

In action notation we represent stable information by a map from storage cells to individual items of storable data.

• Action notation includes a functional action notation for specifying data flow.

• Functional actions are concerned with transient information.

• Chapter 13 illustrates the use of functional action notation in the semantic description of expressions and statements.

So far, we have considered actions and data separately: basic action notation does not involve data at all, nor does data notation involve actions. This chapter introduces functional actions that do involve data, as well as yielders that can occur in actions.

The information that actions can process is classified as transient, scoped, stable, or permanent, according to how far it tends to be propagated. Functional actions are concerned with processing transient information, which generally isn't propagated very far during action performance. The transient information current at the start of an action may still be current at the start of the action's direct subactions. However, almost all primitive actions, and a few combinators, prevent the propagation of transient information, so it usually disappears rather quickly.

Transient information represents intermediate values computed during program execution. For example, it may represent the values of some subexpressions, prior to the application of an arithmetic operation to them. Transient information typically corresponds to data which implementations put in registers, or on a stack.

Each item of transient information consists of a single individual of sort datum. We represent a collection of transients as a tuple, so as to be able to keep track of each item.

• Declarations include definitions of constants and packages. Expressions include identifiers, as well as aggregates for arrays and records and selection of components. Statements include blocks with local declarations.

• The semantic description of declarations, etc., illustrates the use of the declarative action notation introduced in Chapter 7.

• Semantic entities now include general array and record values, and packages.

Declarations in programs are constructs that are similar to mathematical definitions, in that they introduce symbols and determine their interpretation. The symbols introduced are called identifiers. Declarations are said to bind identifiers to their interpretation.

The scope of a declaration is the part of the program in which its binding is valid. This is usually the rest of the block statement in which it occurs, except for inner blocks where the same identifier is re-declared, thus making a hole in the scope of the outer-level declaration. Declarations can also occur in modules, which are called packages in ADA. A module may limit the scope of the declarations in it, and it declares a module identifier which may be used to import the bindings of the declarations into other modules.

The processing of a declaration is called its elaboration. Declarations may involve expressions that are to be evaluated, so their elaboration generally has a computational aspect—in contrast to mathematical definitions.

A record value is similar to a module or package entity, in that its field identifiers can be regarded as bound to component values.

• Expressions include arithmetic and Boolean operations. Statements involving expressions include conditionals, while-loops, and guarded alternatives.

• The semantic description of expressions and statements illustrates the use of the functional action notation introduced in Chapter 6.

• Semantic entities are the same as for literals, although further operations on them are needed now.

Expressions in programming languages resemble mathematical terms. Syntactically, both expressions and terms are generally formed from literal constants, such as numerals, and variables, using mathematical operators, such as +. Semanticaily, both expressions and terms are evaluated to particular values.

There are, however, some distinctive differences between expressions and terms. Function calls in expressions may lead to divergence, whereas the application of a mathematical function in a term to arguments outside its domain of definition is merely undefined. Expression evaluation may even involve execution of statements. The notion of a program variable in an expression is quite different from that of a mathematical variable in a term, as explained in detail in Chapter 15. The order of evaluation of subexpressions in an expression may affect the value given—although in most programming languages, the order of evaluation is deliberately left implementation-dependent, which prevents program(mer)s from relying on any particular order. Whether or not a particular subexpression gets evaluated may also affect the outcome of the evaluation, and some expression constructs conditionally avoid the evaluation of particular subexpressions.

• AD is a medium-scale, high-level programming language. Syntactically, it is a sublanguage of ADA.

• The specified action semantics for AD constructs does not always correspond exactly to the semantics described in the ADA Reference Manual. For instance, parameter passing modes are left implementation-dependent in ADA, but not in AD.

• The action semantic description of AD given here collects and extends the fragmented illustrations given throughout Part III. It also provides the full algebraic specifications of all the semantic entities used in Part III.

• Some of the actions specified in Part III are respecified here with some extra subactions. For example, the action representing the execution of a block statement now synchronizes with locally-declared tasks before starting to execute the block body, and relinquishes locally-declared variables afterwards.

• The description of AD allows assessment of the pragmatic qualities of action semantics: readability, comprehensibility, modularity, modifiability, etc.

• To extend the description of AD to an accurate description of ADA would be a major project, the feasibility of which remains to be seen.

• The modular structure of the description is specified first, in the order in which the modules are presented, which is mostly bottom-up.

In this first part of the book we introduce a few categories as fundamental semantic frameworks and explore the formulation of general choice operators and iteration in arbitrary categories with finite coproducts.

• The specification of the algebraic properties of action notation in this Appendix is divided into modules as shown on the next page.

• The body of each module introduces symbols, highlights their principal properties, and lists their secondary properties.

• The properties specified are sufficient to reduce the full action notation to a kernel, whose abstract syntax and structural operational semantics are defined in Appendix C.

• The specified properties of the kernel action notation hold for the notion of action equivalence defined at the end of Appendix C. The algebraic theory of action notation is not yet fully developed, although it may already be adequate for verifying the semantic correctness of simple program optimizations.

• Action notation supports concurrency, but without introducing a combinator for it, so there are no algebraic properties concerning the sending and receipt of messages, or the fulfilment of contracts.

• The moduleFacetsdeserves special mention. It defines a moderately expressive notation for subsorts of actions, with reference to outcomes and incomes, and similarly for yielders. This notation is specified axiomatically; the expected correspondence with the operational semantics of action notation has not yet been proved. Nevertheless, the axiomatic specification of the subsort notation provides useful documentation of the sorts of yielders to be used in primitive actions, and of the various facets of the action combinators.

• Descriptions of programming languages have several important applications.

• Different applications require different features of descriptions.

• Informal descriptions are inadequate: formality is essential.

• Good pragmatic features are needed to make formal descriptions usefu.

• Comprehensive language descriptions involve both syntax and semantics.

• Standards relate syntax and semantics to implementations.

This chapter provides some background for the main topic of this book, namely the action semantic description of programming languages. We start by identifying some important uses for descriptions of programming languages. Although various uses require different features of descriptions, these requirements are not necessarily conflicting. Formality is a particularly important feature. We go on to consider the factorization of language descriptions into syntax and semantics, and discuss how they relate to the pragmatic issue of setting standards for programming languages.

Motivation

Programming languages are artificial languages. Programs written in them are used to control the execution of computers. There are many programming languages in existence. Some are simple, intended for special purposes; others are complex and general-purpose, for use in a wide variety of applications.

Even though programming languages lack many of the features of natural languages, such as vagueness, it is not at all easy to give accurate, comprehensive descriptions of them. Which applications require descriptions of programming languages—and hence motivate the study of appropriate frameworks for such descriptions?

First, there is the programming language design process.