Dynamic modeling provides a dynamic (also referred to as behavioral) view of a system in which control and sequencing is considered, either within an object (by means of a state machine) or among objects (by analysis of object interactions). Dynamic state machine modeling is described in Chapter 7. This chapter describes dynamic interaction modeling among objects. However, for state dependent control objects, this chapter also describes how state machines are used to help determine state dependent object interactions. Please note that all references to system in this chapter are to the software system.

Dynamic interaction modeling is based on the realization of the use cases developed during use case modeling. For each use case, it is necessary to determine how the objects that participate in the use case dynamically interact with each other. The object structuring criteria described in Chapter 8 are applied to determine the objects that participate in each use case. This chapter describes how, for each use case, an interaction diagram is developed to depict the objects that participate in the use case and the sequence of messages passed between them. The interaction is depicted on either a sequence diagram or a communication diagram. A textual description of the object interaction is also provided in a message sequence description.

There are two main kinds of dynamic interaction modeling. Stateless dynamic interaction modeling is applied if the interaction sequence does not involve a state dependent control object. State dependent dynamic interaction modeling is applied if at least one of the objects is a state dependent control object, in which case the interaction is state dependent and necessitates the execution of a state machine. State dependent dynamic interaction modeling is particularly important in real-time embedded systems, because object interactions in these systems are frequently state dependent.

For large systems, a preliminary determination of the subsystems is usually necessary – for example, based on geographical distribution, as in distributed component-based systems described in Chapter 12. The analysis is then conducted to determine the object communication in each subsystem. Subsystem structuring is carried out in more depth during the design phase as described in Chapter 10.

Section 9.1 gives an overview of object interaction modeling. Section 9.2 describes message sequence descriptions.

Use case modeling is widely used for specifying the functional requirements of software systems. This chapter describes how use case modeling can be applied to real-time embedded systems from both a systems engineering and a software engineering perspective. With use case modeling, the system is viewed as a black box, so that only the external characteristics of the system are considered. Both functional and nonfunctional requirements need to be described for embedded systems. Functional requirements address the functionality that the system needs to provide. Nonfunctional requirements, sometimes referred to as quality attributes, address quality of service goals for the system, which are particularly important for real-time embedded systems. Although use case modeling is typically only used for specifying functional requirements, this chapter describes how it can be extended to specify nonfunctional requirements. Several examples of use case modeling for embedded systems are given in this chapter.

Section 6.1 gives an overview of use case modeling. Section 6.2 then describes actors and their role in use case modeling from both systems engineering and software engineering perspectives. The important topic of how to identify use cases is covered in Section 6.3. Section 6.4 describes how to document use cases. Section 6.5 describes how to specify nonfunctional requirements, which is particularly important for real-time embedded systems. Section 6.6 gives detailed examples of use case descriptions from both systems engineering and software engineering perspectives. Section 6.7 then describes use case relationships; modeling with the include relationship is described in Section 6.8; modeling with the extend relationship is described in Section 6.9. Finally, use case packages for structuring large use case models are described in Section 6.10.

USE CASES

In the use case modeling approach, functional requirements are defined in terms of actors, which are external to the system, and use cases. A use case defines a sequence of interactions between one or more actors and the system. The use case model describes the functional requirements of the system in terms of the actors and use cases. In particular, the use case model considers the system as a black box and describes the interactions between the actor(s) and the system in a narrative textual form consisting of actor inputs and system responses.

Modularity is the most important technique for controlling the complexity of programs. Programs are decomposed into separate components with precisely specified, and tightly controlled, interactions. The pathways for interaction among components determine dependencies that constrain the process by which the components are integrated, or linked, to form a complete system. Different systems may use the same components, and a single system may use multiple instances of a single component. Sharing of components amortizes the cost of their development across systems and helps limit errors by limiting coding effort.

Modularity is not limited to programming languages. In mathematics, the proof of a theorem is decomposed into a collection of definitions and lemmas. References among the lemmas determine a dependency relation that constrains their integration to form a complete proof of the main theorem. Of course, one person's theorem is another person's lemma; there is no intrinsic limit on the depth and complexity of the hierarchies of results in mathematics. Mathematical structures are themselves composed of separable parts, for example, a ring comprises a group and a monoid structure on the same underlying set. Modularity arises from the structural properties of the hypothetical and general judgments. Dependencies among components are expressed by free variables whose typing assumptions state the presumed properties of the component. Linking amounts to substitution to discharge the hypothesis.

Simple Units and Linking

Decomposing a program into units amounts to exploiting the transitivity of the hypothetical judgment (see Chapter 3). The decomposition may be described as an interaction between two parties, the client and the implementor, mediated by an agreed-upon contract, an interface. The client assumes that the implementor upholds the contract, and the implementor guarantees that the contract will be upheld. The assumption made by the client amounts to a declaration of its dependence on the implementor discharged by linking the two parties accordng to their agreed-upon contract.

The interface that mediates the interaction between a client and an implementor is a type. Linking is the implementation of the composite structural rules of substitution The type τintf is the interface type. It defines the operations provided by the implementor eimpl and relied upon by the client eclient.

A symbol is an atomic datum with no internal structure. Whereas a variable is given meaning by substitution, a symbol is given meaning by a family of operations indexed by symbols. A symbol is just a name, or index, for a family of operations. Many different interpretations may be given to symbols according to the operations we choose to consider, giving rise to concepts such as fluid binding, dynamic classification, mutable storage, and communication channels. A type is associated to each symbol whose interpretation depends on the particular application. For example, in the case of mutable storage, the type of a symbol constrains the contents of the cell named by that symbol to values of that type.

In this chapter, we consider two constructs for computing with symbols. The first is a means of declaring new symbols for use within a specified scope. The expression new a ~ ρ in e introduces a “new” symbol a with associated type ρ for use within e. The declared symbol a is “new” in the sense that it is bound by the declaration within e and so may be renamed at will to ensure that it differs from any finite set of active symbols. Whereas the statics determines the scope of a declared symbol, its range of significance, or extent, is determined by the dynamics. There are two different dynamic interpretations of symbols, the scoped and the free (short for scope-free) dynamics. The scoped dynamics limits the extent of the symbol to its scope; the lifetime of the symbol is restricted to the evaluation of its scope. Alternatively, under the free dynamics the extent of a symbol exceeds its scope, extending to the entire computation of which it is a part.We may say that in the free dynamics a symbol “escapes its scope,” but it is more accurate to say that its scope widens to encompass the rest of the computation.

The second construct associated with symbols is the concept of a symbol reference, an expression whose purpose is to refer to a particular symbol. Symbol references are values of a type ρ sym and are written ‘a for some symbol a with associated type ρ. The elimination form for the type ρ sym is a conditional branch that determines whether a symbol reference refers to a statically specified symbol.

Lazy evaluation comprises a variety of methods to defer evaluation of an expression until it is required, and to share the results of any such evaluation among all uses of a deferred computation. Laziness is not merely an implementation device, but it also affects the meaning of a program.

One form of laziness is the by-need evaluation strategy for function application. Recall from Chapter 8 that the by-name evaluation order passes the argument to a function in unevaluated form so that it is only evaluated if it is actually used. But because the argument is replicated by substitution, it might be evaluated more than once. By-need evaluation ensures that the argument to a function is evaluated at most once, by ensuring that all copies of an argument share the result of evaluating any one copy.

Another form of laziness is the concept of a lazy data structure. As we have seen in Chapters 10, 11, and 20, we may choose to defer evaluation of the components of a data structure until they are actually required, and not when the data structure is created. But if a component is required more than once, then the same computation will, without further provision, be repeated on each use. To avoid this, the deferred portions of a data structure are shared so an access to one will propagate its result to all occurrences of the same computation.

Yet another form of laziness arises from the concept of general recursion considered in Chapter 19. Recall that the dynamics of general recursion is given by unrolling, which replicates the recursive computation on each use. It would be preferable to share the results of such computation across unrollings. A lazy implementation of recursion avoids such replications by sharing those results.

Traditionally, languages are biased towards either eager or lazy evaluation. Eager languages use a by-value dynamics for function applications, and evaluate the components of data structures when they are created. Lazy languages adopt the opposite strategy, preferring a by-name dynamics for functions, and a lazy dynamics for data structures. The overhead of laziness is reduced by managing sharing to avoid redundancy. Experience has shown, however, that the distinction is better drawn at the level of types. It is important to have both lazy and eager types, so that the programmer controls the use of laziness, rather than having it enforced by the language dynamics.

Modernized Algol, or MA, is an imperative, block-structured programming language based on the classic language Algol. MA extends PCF with a new syntactic sort of commands that act on assignables by retrieving and altering their contents. Assignables are introduced by declaring them for use within a specified scope; this is the essence of block structure. Commands are combined by sequencing and are iterated using recursion.

MA maintains a careful separation between pure expressions, whose meaning does not depend on any assignables, and impure commands, whose meaning is given in terms of assignables. The segregation of pure from impure ensures that the evaluation order for expressions is not constrained by the presence of assignables in the language, so that they can be manipulated just as in PCF. Commands, on the other hand, have a constrained execution order, because the execution of one may affect the meaning of another.

A distinctive feature of MA is that it adheres to the stack discipline, which means that assignables are allocated on entry to the scope of their declaration, and deallocated on exit, using a conventional stack discipline. Stack allocation avoids the need for more complex forms of storage management, at the cost of reducing the expressive power of the language.

Basic Commands

The syntax of the language MA of modernized Algol distinguishes pure expressions from impure commands. The expressions include those of PCF (as described in Chapter 19), augmented with one construct, and the commands are those of a simple imperative programming language based on assignment. The language maintains a sharp distinction between variables and assignables. Variables are introduced by λ-abstraction and are given meaning by substitution. Assignables are introduced by a declaration and are given meaning by assignment and retrieval of their contents, which is, for the time being, restricted to natural numbers. Expressions evaluate to values, and have no effect on assignables. Commands are executed for their effect on assignables, and return a value. Composition of commands not only sequences their execution order, but also passes the value returned by the first to the second before it is executed. The returned value of a command is, for the time being, restricted to the natural numbers.

Programming languages express computations in a form comprehensible to both people and machines. The syntax of a language specifies how various sorts of phrases (expressions, commands, declarations, and so forth) may be combined to form programs. But what are these phrases? What is a program made of?

The informal concept of syntax involves several distinct concepts. The surface, or concrete, syntax is concerned with how phrases are entered and displayed on a computer. The surface syntax is usually thought of as given by strings of characters from some alphabet (say, ASCII or Unicode). The structural, or abstract, syntax is concerned with the structure of phrases, specifically how they are composed from other phrases. At this level, a phrase is a tree, called an abstract syntax tree, whose nodes are operators that combine several phrases to form another phrase. The binding structure of syntax is concerned with the introduction and use of identifiers: how they are declared, and how declared identifiers can be used. At this level, phrases are abstract binding trees, which enrich abstract syntax trees with the concepts of binding and scope.

We will not concern ourselves in this book with concrete syntax but will instead consider pieces of syntax to be finite trees augmented with a means of expressing the binding and scope of identifiers within a syntax tree. To prepare the ground for the rest of the book, we define in this chapter what is a “piece of syntax” in two stages. First, we define abstract syntax trees, or ast's, which capture the hierarchical structure of a piece of syntax, while avoiding commitment to their concrete representation as a string. Second, we augment abstract syntax trees with the means of specifying the binding (declaration) and scope (range of significance) of an identifier. Such enriched forms of abstract syntax are called abstract binding trees, or abt's for short.

Several functions and relations on abt's are defined that give precise meaning to the informal ideas of binding and scope of identifiers. The concepts are infamously difficult to define properly and are the mother lode of bugs for language implementors. Consequently, precise definitions are essential, but they are also fairly technical and take some getting used to. It is probably best to skim this chapter on first reading to get the main ideas, and return to it for clarification as necessary.

In constructive logic, a proposition is true exactly when it has a proof, a derivation of it from axioms and assumptions, and is false exactly when it has a refutation, a derivation of a contradiction from the assumption that it is true. Constructive logic is a logic of positive evidence. To affirm or deny a proposition requires a proof, either of the proposition itself, or of a contradiction, under the assumption that it has a proof. We are not always able to affirm or deny a proposition. An open problem is one for which we have neither a proof nor a refutation—constructively speaking, it is neither true nor false.

In contrast, classical logic (the one we learned in school) is a logic of perfect information where every proposition is either true or false.We may say that classical logic corresponds to “god's view” of the world—there are no open problems, rather all propositions are either true or false. Put another way, to assert that every proposition is either true or false is to weaken the notion of truth to encompass all that is not false, dually to the constructively (and classically) valid interpretation of falsity as all that is not true. The symmetry between truth and falsity is appealing, but there is a price to pay for this: the meanings of the logical connectives are weaker in the classical case than in the constructive.

The law of the excluded middle provides a prime example. Constructively, this principle is not universally valid, as we have seen in Exercise 12.1. Classically, however, it is valid, because every proposition is either false or not false, and being not false is the same as being true. Nevertheless, classical logic is consistent with constructive logic in that constructive logic does not refute classical logic. As we have seen, constructive logic proves that the law of the excluded middle is positively not refuted (its double negation is constructively true). Consequently, constructive logic is stronger (more expressive) than classical logic, because it can express more distinctions (namely, between affirmation and irrefutability), and because it is consistent with classical logic.

Proofs in constructive logic have computational content: they can be executed as programs, and their behavior is described by their type. Proofs in classical logic also have computational content, but in a weaker sense than in constructive logic.

Constructive logic codifies the principles of mathematical reasoning as it is actually practiced. In mathematics a proposition is judged true exactly when it has a proof, and is judged false exactly when it has a refutation. Because there are, and always will be, unsolved problems, we cannot expect in general that a proposition is either true or false, for in most cases, we have neither a proof nor a refutation of it. Constructive logic can be described as logic as if people matter, as distinct from classical logic, which can be described as the logic of the mind of god.

From a constructive viewpoint, a proposition is true when it has a proof.What is a proof is a social construct, an agreement among people as to what is a valid argument. The rules of logic codify a set of principles of reasoning that may be used in a valid proof. The valid forms of proof are determined by the outermost structure of the proposition whose truth is asserted. For example, a proof of a conjunction consists of a proof of each conjunct, and a proof of an implication transforms a proof of its antecedent to a proof of its consequent. When spelled out in full, the forms of proof are seen to correspond exactly to the forms of expression of a programming language. To each proposition is associated the type of its proofs; a proof is then an expression of the associated type. This association between programs and proofs induces a dynamics on proofs. In this way, proofs in constructive logic have computational content, which is to say that they are interpreted as executable programs of the associated type. Conversely, programs have mathematical content as proofs of the proposition associated to their type.

The unification of logic and programming is called the propositions as types principle. It is a central organizing principle of the theory of programming languages. Propositions are identified with types, and proofs are identified with programs. A programming technique corresponds to a method of proof; a proof technique corresponds to a method of programming. Viewing types as behavioral specifications of programs, propositions are problem statements whose proofs are solutions that implement the specification.