ACM Transactions on Programming Languages and Systems

Inheritance is well-known and accepted as a mechanism for reuse in object-oriented languages. Unfortunately, due to the coarse granularity of inheritance, it may be difficult to decompose an application into an optimal class hierarchy that maximizes software reuse. Existing schemes based on single inheritance, multiple inheritance, or mixins, all pose numerous problems for reuse. To overcome these problems we propose traits , pure units of reuse consisting only of methods. We develop a formal model of traits that establishes how traits can be composed, either to form other traits, or to form classes. We also outline an experimental validation in which we apply traits to refactor a nontrivial application into composable units.

Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.

We present a static analysis technique for nontermination inference of logic programs. Our framework relies on an extension of the subsumption test, where some specific argument positions can be instantiated while others are generalized. We give syntactic criteria to statically identify such argument positions from the text of a program. Atomic left looping queries are generated bottom-up from selected subsets of the binary unfoldings of the program of interest. We propose a set of correct algorithms for automating the approach. Then, nontermination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. An experimental evaluation is reported and the analyzers can be tried online at http://www.univ-reunion.fr/~gcc. When termination and nontermination analysis produce complementary results for a logic procedure, then with respect to the leftmost selection rule and the language used to describe sets of atomic queries, each analysis is optimal and together, they induce acharacterizationof the operational behavior of the logic procedure.

The ASF+SDF Meta-Environment is an interactive language development environment whose main application areas are definition and implementation of domain-specific languages, generation of program analysis and transformation tools, and production of software renovation tools. It uses conditional rewrite rules to define the dynamic semantics and other tool-oriented aspects of languages, so the effectiveness of the generated tools is critically dependent on the quality of the rewrite rule implementation. The ASF+SDF rewrite rule compiler generates C code, thus taking advantage of C's portability and the sophisticated optimization capabilities of current C compilers as well as avoiding potential abstract machine interface bottlenecks. It can handle large (10,000+ rule) language definitions and uses an efficient run-time storage scheme capable of handling large (1,000,000+ node) terms. Term storage uses maximal subterm sharing (hash-consing), which turns out to be more effective in the case of ASF+SDF than in Lisp or SML. Extensive benchmarking has shown the time and space performance of the generated code to be as good as or better than that of the best current rewrite rule and functional language compilers.

The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician's toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.

Designing data types in isolation is fundamentally different from designing them for integration into communities of data types, especially when inheritance is a fundamental issue. Moreover, we can distinguish between the design of families—integrated types that are variations of each other—and more general communities where totally different but cohesive collections of types support specific applications (e.g., a compiler). We are concerned with the design of integrated families of data types as opposed to individual data types; that is, on the issues that arise when the focus is intermediate between the design of individual data types and more general communities of data types. We argue that design at this level is not adequately served by systems providing only class-based inheritance hierarchies and that systems which additionally provide a coupled subtype specification hierarchy are still not adequate. We propose a system that provides an unlimited number of uncoupled specification hi erarchies and illustrate it with three: a subtype hierarchy, a specialization/generalization hierarchy, and a like hierarchy. We also resurrect a relatively unknown Smalltalk design methodology that we call programming-by-exemplars and argue that it is an important addition to a designer's grab bag of techniques. The methodology is used to show that the subtype hierarchy must be decoupled from the inheritance hierarchy, something that other researchers have also suggested. However, we do so in the context of exemplar-based systems to additionally show that they can already support the extensions required without modification and that they lead to a better separation between users and implementers, since classes and exemplars can be related in more flexible ways. We also suggest that class-based systems need the notion of private types if they are to surmount their current limitations. Our points are made in the guise of designing a family of List data types. Among these is a new variety of lists that have never been previously published: prefix-sharing lists. We also argue that there is a need for familial classes to serve as an intermediary between users and the members of a family.

There is a significant class of operations such as mapping that are common to all data structures. The goal of generic programming is to support these operations on arbitrary data types without having to recode for each new type. The pattern calculus and combinatory type system reach this goal by representing each data structure as a combination of names and a finite set of constructors. These can be used to define generic functions by pattern-matching programs in which each pattern has a different type. Evaluation is type-free. Polymorphism is captured by quantifying over type variables that represent unknown structures. A practical type inference algorithm is provided.

Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs. This approach regards program synthesis as a theorem-proving task and relies on a theorem-proving method that combines the features of transformation rules, unification, and mathematical induction within a single framework.

We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 10 ¹³⁰⁰ states.