In this chapter we develop an algebraic semantics for modal logic. The basic idea is to extend the algebraic treatment of classical propositional logic (which uses boolean algebras) to modal logic. The algebras employed to do this are called boolean algebras with operators (BAOs). The boolean part handles the underlying propositional logic, the additional operators handle the modalities.

But why algebraize modal logic? There are two main reasons. First, the algebraic perspective allows us to bring powerful new techniques to bear on modal-logical problems. Second, the algebraic semantics turns out to be better-behaved than frame-based semantics: we will be able to prove an algebraic completeness result for every normal modal logic. As our discussion of incompleteness in Section 4.4 makes clear, no analogous result holds for frames.

This chapter has three main parts. The first, consisting of the first three sections, introduces the algebraic approach: we survey the basic ideas in the setting of classical propositional logic, extend them to modal logic, and prove the Jónsson-Tarski Theorem. The second part, which consists of the fourth section, introduces duality theory, the study of correspondences between the universe of algebras and the universe of frames. The last part (the only part on the advanced track) is devoted to general frames. These turn out to be set-theoretic representations of boolean algebras with operators, and we examine their properties in detail, and use them to prove the Sahlqvist Completeness Theorem. Background information on universal algebra can be found in Appendix B.

As promised in the preface, this chapter is the party at the end of the book. We have chosen six of our favorite topics in extended modal logic, and we are going to tell you a little about them. There is no point in offering detailed advice here: simply read these introductory remarks and the following Chapter Guide and turn to whatever catches your fancy.

Roughly speaking, the chapter works its way from fairly concrete to more abstract. A recurrent theme is the interplay between modal and first-order ideas. We start by introducing a number of important logical modalities (and learn that we have actually been using logical modalities all through the book). We then examine languages containing the since and until operators, and show that first-order expressive completeness can be used to show modal deductive completeness. We then explore two contrasting strategies, namely the strategy underlying hybrid logic (import first-order ideas into modal logic, notably the ability to refer to worlds) and the strategy that leads to the guarded fragment of first-order logic (export the modal locality intuition to classical logic). Following this we discuss multi-dimensional modal logic (in which evaluation is performed at a sequence of states), and see that first-order logic itself can be viewed as modal logic. We conclude by proving a Lindström Theorem for modal logic.

Chapter guide

Section 7.1: Logical Modalities (Basic track). Logical modalities have a fixed interpretation in every model.

Languages of propositional modal logic are propositional languages to which sentential operators (usually called modalities or modal operators) have been added. In spite of their syntactic simplicity, such languages turn out to be useful tools for describing and reasoning about relational structures. A relational structure is a non-empty set on which a number of relations have been defined; they are widespread in mathematics, computer science, artificial intelligence and linguistics, and are also used to interpret first-order languages.

Now, when working with relational structures we are often interested in structures possessing certain properties. Perhaps a certain transitive binary relation is particularly important. Or perhaps we are interested in applications where ‘dead ends,’ ‘loops,’ and ‘forkings’ are crucial, or where each relation is a partial function. Wherever our interests lie, modal languages can be useful, for modal operators are essentially a simple way of accessing the information contained in relational structures. As we will see, the local and internal access method that modalities offer is strong enough to describe, constrain, and reason about many interesting and important aspects of relational structures.

Much of this book is essentially an exploration and elaboration of these remarks. The present chapter introduces the concepts and terminology we will need, and the concluding section places them in historical context.

Chapter guide

Section 1.1: Relational Structures. Relational structures are defined, and a number of examples are given.

Section 1.2: Modal Languages. We define the basic modal language and some of its extensions.

In this appendix we introduce the basic ideas of computability theory (the study of which problems are, and which problems are not, computationally solvable), and provide some background information on complexity theory (the study of the computational resources required to solve problems).

For detailed discussions of computability, see Rogers [391] or Odifreddi [343]. For accessible introductions to the subject, see Boolos and Jeffrey [70], or Cutland [103]. But the single most useful source is probably the (second edition of) Lewis and Papadimitriou [301]; this introduces computability theory, and then goes on to treat computational complexity. For more on computational complexity, try Garey and Johnson [163] and Papadimitriou [352]. Garey and Johnson's book is a source for information on NP-complete problems, but it discusses the basic ideas of computational complexity lucidly, and gives background information on other complexity classes. Papadimitriou's book is a well-written introduction to computational complexity covering far more than is needed to understand Chapter 6; if you want to go deeper into computational complexity, it is a good place to start.

Computability and Uncomputability

To prove theorems about computability — and in particular to prove that some problem is not computable — we need a robust mathematical model of computability. One of the most widely used models is the Turing machine. A Turing machine is a device which manipulates symbols written on a tape. The symbols are taken from some alphabet fixed in advance (often the alphabet simply consists of the two symbols 0 and 1).

In this book we've talked a lot about programming using ENVY System classes. At the simplest level this involves implementing methods such as loaded or removing on our own application classes. At the most complex level, we've seen code to create checkpoint versions directly out of application editions in the repository. All of this requires manipulating the classes that make up ENVY itself.

This kind of programming can be quite difficult. Although we refer to this as an API, many of these classes and methods are not well documented and have changed over time. The most difficult part of writing ENVY system code is understanding the relationships between components and finding the methods necessary to manipulate these relationships. This is complicated by a few factors. First, the components are not directly related through instance variables; rather, many of the most important relationships are implicit in methods. Further, these methods are not concentrated in the components themselves, but are spread out over three distinct groups of classes: the browsers, the “helper” classes such as EmInterface, and the components themselves.

In the earliest versions of ENVY almost everything was done directly in the browser code. Over time much of the code was moved to the components themselves or to utility classes such as EtTools and EmInterface. This reduced code duplication but the utility classes became very complex, with many methods that manipulate different types of components, making it harder to find any given piece of functionality.

So far, we've seen ENVY as a code organizing tool and as a version control system. These are powerful facilities, but the most important aspects of ENVY are in its support for working in teams. ENVY differs from traditional team programming tools in many respects. Because it is a Smalltalk-based tool it can deal with software components as objects, rather than working with coarse-grained source files. It also breaks away from the check-in/check-out mechanisms to a more concurrent mechanism in which conflicts are resolved through component ownership and through separation of the versioning and releasing operations. This enables developers to work with maximum concurrency while still providing a disciplined process that maintains the consistency of the system.

Team Development with Class Editions

Recall that applications specify a group of class versions that are loaded when the application is loaded, and that these are called the released versions. As we look at team development, this concept becomes more important, and we will see how class and application editions and versions are used to control the team development process.

Before we begin, let's review what it means for a class version to be released:

1. ▪ When an application edition is loaded, the released versions of its classes are automatically loaded.

2. ▪ Once an application is versioned, the list of released class versions cannot be modified.

3. ▪ Most important, the released version is the approved or official edition. If we release a class, we are saying it is stable enough and approved for other developers to use.

In a software project, as in any large project, a significant amount of work is needed to close the project. Teams often defer the hard issues of finally delivering a product until much too late in the process, leading to trouble when the time finally arrives.

This chapter examines the ENVY notion of prerequisites in depth, sees how it can affect packaging, and looks at resolving various prerequisite problems. We will look at various alternatives for the packaging and delivery process and their relative advantages and disadvantages. We'll describe in some detail the packaging and delivery process for both VisualAge and VisualWorks. We'll look at application attachments, an ENVY mechanism for keeping track of external files associated with our program. Finally, we'll address some additional delivery issues and strategies for ensuring that packaging does not become a bottleneck.

Prerequisites Revisited

Before we examine program delivery strategies, it's worth revisiting some of the concepts we've previously seen that have a significant effect on delivery. Regardless of our strategy, knowing what other code our program relies on is important if we are to produce a simple, standalone program. Recall that ENVY provides the notion of application prerequisites to help formalize this information. Some packaging strategies, particularly those using the VisualAge packager, rely heavily on correct prerequisites to determine which components need to be linked and which classes and methods can be discarded. Even if we're not using such a mechanism, ENVY prerequisites can help define a layered architecture with all the dependencies made clear.

This is the chapter to read when you have trouble. We'll discuss dealing with components that won't load, recovering from simple image crashes as well as more complex ENVY crashes, and what you can do to make recovery easier. We'll also discuss more generic project troubleshooting to help you identify potential ENVY-related problems in a project, and suggest some possible remedies. The main topics we won't discuss here are installation and configuration problems, which we covered in Chapter 1.

Component Loading

One of the most common ENVY problems is that component editions will not load. A load may fail for many reasons. Two of the most common reasons are that a component cannot be constructed in the image (for example, the source for a method cannot be compiled or a required superclass is missing), or that loading a component results in the image being inconsistent (for example, a subapplication, class, or method would exist in two different places).

You have three main approaches to correcting a load failure, depending on the situation:

1. ▪ altering an ENVY system setting that affects loading behavior

2. ▪ modifying the component editions being loaded

3. ▪ modifying the image

In the previous chapters we've rapidly covered almost everything you need to do basic development with ENVY. This chapter deals with some of the more complex issues that arise in a larger project. The two primary issues we'll address are configuration management and project organization. ENVY supports sophisticated configuration management that enables us to write portable software that can also exploit platform features. Project organization includes advice on how to structure the ENVY components that make up a project, a discussion of multi-site development, and ways to manage multiple divergent streams. We also discuss some alternative processes to the standard we've been describing so far, explaining how ENVY can be used as part of an “Extreme Programming” project. Finally, we'll add some miscellaneous topics, tricks, and conventions that ease development.

The discussion here is aimed at someone who has a good understanding of the basic ENVY concepts and has used ENVY at least a little. Much of this advice will be most helpful to someone setting up a larger project. New users should begin by reading some of the previous chapters and working with the concepts discussed in those chapters. Toolsmiths will find this discussion important for ways to organize tools for multiple versions or dialects, and will appreciate some of the tips and conventions.

Configuration Management

The distinction between version control and configuration management is not clearly drawn. However, in our context we will identify configuration management as being concerned with variations in our software due to different configuration information.

This book describes ENVY/Developer and its use by three very experienced professional software developers who have used it to build both successful products, including Top Link and VA/Java, and applications for numerous customers. Their unique user-oriented perspectives give developers and managers insight into how to use the product successfully in team development projects.

ENVY/Developer began as Orwell (OOPSLA reference), a research prototype developed in the Object Oriented Research Group, at Carleton University. It was built as part of the Actra project; a multiprocessor embedded Smalltalk, funded by the Defense Research Establishment Ottawa. Orwell addressed the problem of coordinating multiple developers working in the OO RAD environment of Smalltalk.

In designing Orwell, we sought to address the needs of our funding agency DREO, in particular Dr. Brian Barry who would later become CTO, then CEO of Object Technology International (OTI) and was interested in versioning configuration management for Smalltalk. Our goal was to meet the needs of our development team, which meant preserving the incremental nature of the Smalltalk programming environment.

What we developed at Carleton, then quickly re-implemented at OTI, was a strong specific solution for Smalltalk. Little did we know at the time how strong and specific it was to be! It was developed as an internal tool to support building embedded systems, hence the strict rules for compatibility, which were designed to reduce the downstream problems of the packaging or roaming engineer.

Smalltalk was first built as a personal computing environment. Most systems at that time were time-sharing, with character-based terminals. In contrast, Smalltalk provided a high-resolution graphical screen and a mouse to maximize the power available to the one user actually sitting at the machine. Smalltalk was designed so that every component in the system was accessible to the user and could be understood by one person.

This was an outstanding vision, and one that remains both important and ahead of the mainstream even today. However, this emphasis on the personal meant that cooperative development issues were less well represented.

Individuals could be incredibly productive, but the code resided in each developer's image and was not directly visible to other team members. The code could be filed out and exchanged between developers but on an ad hoc basis. The way Smalltalk represented code, and the development practices that Smalltalk encouraged were not a good match for the file-based version control systems of the day. As Smalltalk became more widely used in industry, the need for support of large teams became more critical.

Different schemes were attempted that built relatively lightweight Smalltalk layers on top of existing team programming systems. Finally, in the mid-1980s, Carleton University Professor Dave Thomas and some of his students broke the mold and came up with Orwell, a repository-based system that was tightly integrated with the Smalltalk environment.

The previous four chapters have described ENVY concepts in a tutorial form, helpful for developers getting started with ENVY and advanced developers looking for detailed information and motivation for features. In this chapter we take a different approach, describing the ENVY feature set in a more formal way. This is more appropriate for readers with a background in configuration management seeking to understand the differences between ENVY and other systems. It's also appropriate for users familiar with ENVY who want to understand more about the theoretical motivations behind certain features. This chapter covers most of the material explained in the previous four chapters but in less detail and from a more theoretical perspective.

ENVY Products

Technically, ENVY is a generic term for an entire product line from Object Technology International (OTI). Most commonly, it is used to refer to the team programming environment ENVY/Manager. ENVY/Manager has existed for a variety of different Smalltalk environments. It was originally written for Digitalk's Smalltalk/V line, ported to ParcPlace's VisualWorks (now owned by Cincom Systems), and was then tightly integrated into IBM's VisualAge product line, supporting both the Smalltalk and Java versions. In this chapter we use the term ENVY to refer to the ENVY/Manager environment, as it exists for VisualWorks and VisualAge Smalltalk.

Components

The fundamental concept in ENVY is that of software components. We will begin introducing the different types of components: applications, subapplications, classes, class extensions, and configuration maps.

Smalltalk is a wonderfully open environment. Some or all of the source code is available to developers, and can be changed to do almost anything. From an experimental point of view this is wonderful. We can “burn the disk packs” and invent our own new language and environment. Unfortunately, the people who are paying us may have more prosaic goals in mind.

Our changes may need to be reviewed every time there's an upgrade or a patch to the basic class libraries. Inadequately tested extensions can be more trouble than they're worth, and managers of large projects with many developers are often reluctant to have every developer soup up his or her personal environment.

If we make changes to base classes, they may conflict with third-party products, with other teams in the organization, or even with customers if we're distributing development tools. System changes also scatter code around. If we modify a class in Kernel, then our system's configuration map will have to include our special version of Kernel. Before long we're loading dozens of applications, each containing only a few lines of our code. These all have to be managed by Library Supervisor, complicating maintenance.

On the other hand, changing system code offers very significant advantages. Sometimes the system is wrong. It may have bugs, or be missing functionality that requires changes to existing classes. Power-users like to extend their environments because it makes them more productive.