ACM Computing Surveys 28(4es), December 1996, http://www.acm.org/pubs/citations/journals/surveys/1996-28-4es/a48-miller/. Copyright © 1996 by the Association for Computing Machinery, Inc. See the permissions statement below. This article derives from a position statement prepared for the Workshop on Strategic Directions in Computing Research.


Logical Foundations for Open System Design

A position paper


Dale Miller

University of Pennsylvania, Department of Computer Science
200 S. 33rd Street, Philadelphia PA 19104-6389 USA
dale@saul.cis.upenn.edu, http://www.cis.upenn.edu/~dale/


Abstract: Process calculus and linear logic can be applied to some important problems in the design of large-scale software systems. Three general problem areas for applications are outlined.

It is common to contrast two broad approaches to organizing software systems. In a hierarchical organization, components of a software system are viewed as having many inputs and a single output. Such systems are often modeled using functions and generalizations of functions, such as module functors, and their static properties are usually modeled using types and generalizations of types, such as module signatures. The logic behind hierarchical structuring is generally based on intuitionistic logic and the lambda-calculus, and this logic has helped to design and rationalize various successful programming languages and module systems. Hierarchical systems and associated languages are generally sequential in their design (although they may have parallel implementations) and the scope of abstractions remain entirely internal to the function or module in which they are declared.

By contrast, in an open organization, components can have multiple outputs as well as multiple inputs. Examples of such systems are those programming languages and module systems that incorporate such features as object orientation, threads, communication, and even imperative features of programming languages. The theoretical foundations for open organization appears to be much less well understood and developed than for hierarchical systems. To understand a component in such a system, one needs to understand its interactions with an environment. Furthermore, the scope of an abstraction may leave its lexically determined boundary and wander out into the environment: examples of such abstractions are the pi-calculus's scope extrusion and references in SML. Clearly, the logic of such systems is challenging to understand.

These characteristics of open systems are, however, familiar to those working in process calculus, especially more recent calculi that involve value passing and mobility. The theoretical concepts of observational equivalences and bisimulations developed in the concurrency-theory community should find broad application in open systems. Logic-based systems are not commonly used here, although linear logic has recently been used to provide a foundation for both function programming style specification (in the style of Girard and Abramsky) and logic programming style specification (multiset rewriting and the Forum specification language). Below we elaborate on some possible applications of these two formalisms to the problems of open system design and theory in the hope of achieving solutions as successful and canonical as used with hierarchical systems.

Processes as a Common Abstraction

Integrating different programming paradigms is a difficult task for program designers and theoreticians. There are currently numerous paradigms that find important areas of application: for example, imperative (such as C, Ada), object-oriented (Smalltalk, C++), functional (Lisp, SML), and logic (Prolog, lambda Prolog) programming. Within each paradigm, it is generally not difficult to come up with sensible mechanisms for having different programming languages communicate. Thus, for example, it is not uncommon to find robust integration of, say, C and other imperative languages. It has turned out, however, to be difficult to tightly integrate combinations of programs written in different paradigms.

The main problem with such integration is that there is no common semantic model for these different paradigms. Although much work has been done to try to find such models, solutions often are unsatisfactory. For example, the foundations of logic programming and functional programming have been brought together, but the resulting foundation accounts for a language that has a much richer and more complex behavior than either language separately. Instead of trying to find a common declarative semantics that might underlie different paradigms, it would seem fruitful to design a model of operational semantics into which the different paradigms can be encoded, compared, and integrated.

One choice for such an operational semantics would be to use some existing process calculus. Some success in this direction has been achieved by codings into the pi-calculus: Milner coded the operational semantics of lambda-term evaluation; Sangiorgi established properties about evaluation from this encoding; D. Walker coded a simple object-oriented language; B. Li coded large parts of Prolog in a clear and modular fashion; and Chirimar coded various imperative features preserving important semantic notions.

Linear logic appears to provide a second choice for the presentation of operational semantics. Miller has shown how all of linear logic can be seen as a rich and expressive logic programming language, which he named Forum. Most pi-calculus specifications can be carried over to Forum: in the logic setting, however, there are more possibilities of high-level abstractions (such as abstract datatypes). Examples of specifications in Forum include the specification of state in Algol and SML, the concurrency primitives of Concurrent ML, proof search for object-level logics, some simple object-oriented languages, and the pipeline semantics of the DLX RISC processor. A specification of call-by-value evaluation, references, exceptions, and continuation passing has been developed by Chirimar using Forum. He was able to provide a more modular specification than the one given in, say, the definition of SML. Using a logical formalism as a basis allowed him to show various properties of (object-level) programs by simple reasoning with the proof theory of linear logic.

Capturing Exceptional Behaviors in Interfaces

One of the challenges in using off-the-shelf software is that all of that software's behaviors need to be accounted, and generally only its input-output (functional) behavior is described carefully in interface descriptions (following hierarchical design principles). Seldom does an interface language formally describe the exceptional behaviors that a program might produce or those behaviors that deal with persistent store (files) or global variables. For example, a program that sorts a list of strings might have an interface that merely says that it takes an argument that is a list of strings and outputs a value that is a sorted list of strings: this is the input-output behavior of the program. This sort program, however, may have behaviors that are not captured so simply. For example, the program may choose to allocate a temporary file into which it places some of its strings: thus one of its behaviors would be the allocation of a new file. Such a behavior might be important to know since it is possible that such an allocation request could cause an error if no disk is available or if the disk is full. Other examples of such behaviors include: does the software pop up windows to request additional parameters or display logs; does it raise exceptions when encountering difficult or unexpected problems; does it set and/or read global variables; does it locate customizing parameters in some configuration file; and does it spawn off processes that persist after it completes?

These kinds of items can be considered elements of a program's static semantics. Given the success of process calculus and linear logic in capturing dynamic semantics, their application to static semantics should also be explored. Thus, it is important to design an interface language that attempts to capture all of a software's behavior. Of course, documentation of software generally describes most of the exceptional behaviors of software, but these descriptions are not formalized and amenable to automatic checking and analysis. The use of processes as a common abstraction and of linear logic as a rich setting to specify process behavior should help us develop more comprehensive interface languages.

Formal Manipulation of Interfaces

If one software package provides certain functionality and services and another package needs certain functionality and services, how can a match be determined between them? Clearly, it is not feasible to examine the code within the packages directly to answer this question. The problem of confirming if one module provides what another module requires can be seen as a problem in formal reasoning about the static semantics that form the interface of modules. For example, in many existing languages, this notion of match is particularly simple and inflexible: the offering interface is either identical to or contained in the accepting interface. As types and interfaces become richer and more general, the problem of matching interfaces must also be richer and more flexible.

Intuitionistic and linear logics provide exciting candidates for generalizations of existing matching procedures. For example, in the subsection above on searching libraries, type equivalences were used to extend the matching of a key to a function satisfying that key. Those type equivalences are examples of intuitionistic logic equivalences. For example, it is natural to extend signature matching to allow the matching of requirements if they can be equivalence up to intuitionistic equivalences.

Types based on intuitionistic logic are adequate for abstracting the input-output behavior of pure functional programs but, as described above, are not suited to capturing communications and side effects. Some work on capturing these aspects of a program's meaning has been done in the types and effects setting. Linear logic (in the form of Forum specifications, for example) should allow a logically clean way to specify and reason about a computation's type as well as its possible effects. Linear logic would then provide a framework to compare interface specifications.

Some Links