Adaptive computing systems automatically monitor their behavior and dynamically adjust their own configuration parameters—or knobs—to ensure that user goals are met despite unpredictable external disturbances to the system. A major limitation of prior adaptation frameworks is that their internal adaptation logic is implemented for a specific, narrow set of goals and knobs, which impedes the development of complex adaptive systems that must meet different goals using different sets of knobs for different deployments, or even change goals during one deployment.

Concurrent programming is becoming more important due to the growing dominance of multi-core processors and the prevalence of graphical user interfaces (GUIs). To prepare students for the concurrent future, instructors have begun to address concurrency earlier in their curricula. Unfortunately, test-driven development, which enables students and practitioners to quickly develop reliable single-threaded programs, is not as effective in the domain of concurrent programming. This paper describes how ConcJUnit can simplify the task of writing unit tests for multi-threaded programs, and provides examples that can be used to introduce students to concurrent programming.

Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site. This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.

Developing a general component system for a statically typed, object-oriented language is a challenging design problem for two reasons. First, mutually recursive references across components are common in object-oriented programs-an issue that has proven troublesome in the context of component systems for functional and procedural languages. Second, inheritance across component boundaries can cause accidental method overrides. Our recent research shows that a component framework can be constructed for a nominally typed object-oriented language supporting first-class generic types simply by adding appropriate annotations, syntactic sugar, and component-level type-checking. The fundamental semantic building blocks for constructing, type-checking and manipulating components are provided by the underlying first-class generic type system. To demonstrate the simplicity and utility of this approach we have designed and implemented an extension of Java called Component NEXTGEN (CGEN). CGEN, which is based on the Sun Java 5.0 javac compiler, is backwards compatible with existing Java binary code and runs on current Java Virtual Machines. The primary contribution of this paper is a technical analysis of the subtle design issues involved in building a component framework for a nominally typed object-oriented language supporting first-class generics. In contrast to component systems for structurally typed languages, mutual recursion among components is accommodated in the type system and semantics without incorporating any special machinery. Our analysis includes a presentation of Core CGEN (CCG), a small, core language modeling the CGEN framework. It is based on Featherweight GJ and incorporates some ideas from MIXGEN. CCG adds the essential features to support components, but nothing more. Our discussion includes the type rules and semantics for CCG, as well as a proof of type safety.

Java is the canonical language for teaching introductory programming, but its complex syntax and abundance of constructs are difficult for beginners to learn. This paper shows how object-oriented programming in Java can be made more accessible to beginners through the use of "language levels", a hierarchy of progressively richer subsets of Java. This hierarchy is implemented as an extension of the DrJava pedagogic programming environment.

This paper describes how to add first-class generic types---including mixins---to strongly-typed OO languages with nominal subtyping such as Java and C#. A generic type system is "first-class" if generic types can appear in any context where conventional types can appear. In this context, a mixin is simply a generic class that extends one of its type parameters, e.g., a class C that extends T. Although mixins of this form are widely used in Cpp (via templates), they are clumsy and error-prone because Cpp treats mixins as macros, forcing each mixin instantiation to be separately compiled and type-checked. The abstraction embodied in a mixin is never separately analyzed.Our formulation of mixins using first-class genericity accommodates sound local (class-by-class) type checking. A mixin can be fully type-checked given symbol tables for each of the classes that it directly references---the same context in which Java performs incremental class compilation. To our knowledge, no previous formal analysis of first-class genericity in languages with nominal type systems has been conducted, which is surprising because nominal subtyping has become predominant in mainstream object-oriented programming languages.What makes our treatment of first-class genericity particularly interesting and important is the fact that it can be added to the existing Java language without any change to the underlying Java Virtual Machine. Moreover, the extension is backward compatible with legacy Java source and class files. Although our discussion of a practical implementation strategy focuses on Java, the same implementation techniques could be applied to other object-oriented languages such as C# or Eiffel that support incremental compilation, dynamic class loading, and nominal subtyping.

Students in programming courses generally write "toy" programs that are superficially tested, graded, and then discarded. This approach to teaching programming leaves students unprepared for production programming because the gap between writing toy programs and developing reliable software products is enormous.This paper describes how production programming can be effectively taught to undergraduate students in the classroom. The key to teaching such a course is using Extreme Programming methodology to develop a sustainable open source project with real customers, including the students themselves. Extreme Programming and open source project management are facilitated by a growing collection of free tools such as the JUnit testing framework, the Ant scripting tool, and the SourceForge website for managing open source projects.

DrJava is a pedagogic programming environment for Java that enables students to focus on designing programs, rather than learning how to use the environment. The environment provides a simple interface based on a "read-eval-print loop" that enables a programmer to develop, test, and debug Java programs in an interactive, incremental fashion. This paper gives an overview of DrJava including its pedagogic rationale, functionality, and implementation.

Most software metrics measure the syntactic qualities of a program. While measuring such properties may reveal problems in programs, these metrics fail to measure the essence of programs: (partial) correctness and robustness. We therefore propose to base metrics on semantic, instead of syntactic, criteria. To illustrate the idea of semantics-based metrics, we have built static debuggers, which are tools that detect potential run-time failures. More specifically, a static debugger analyses programs written in safe programming languages and pinpoints those program operations that might trigger a run-time error. This paper briefly recalls what safety means for a programming language. It then sketches how a static debugger works and the role it plays in measuring the robustness of a program. The last section discusses the use of static debuggers in the classroom, an NSF Educational Innovation Project.

The most serious impediment to writing substantial programs in the Java™ programming language is the lack of a gentricity mechanism for abstracting classes and methods with respect to type. During the past two years, several research groups have developed Java extensions that support various forms of genericity, but none has succeeded in accommodating general type parameterization (akin to Java arrays) while retaining compatibility with the existing. Java Virtual Machine. In this paper, we explain how to support general type parameterization---including both non-variant and covariant subtyping---on top of the existing Java Virtual Machine at the cost of a larger code footprint and the forwarding of some method calls involving parameterized classes and methods. Our language extension is forward and backward compatible with the Java 1.2 language and run-time environment: programs in the extended language will run on existing Java 1.2 virtual machines (relying only on the unparameterized Java core libraries) and all existing Java 1.2 programs have the same binary representation and semantics (behavior) in the extended language.

Asoft type systeminfers types for the procedures and data structures of dynamically typed programs. Like conventional static types, soft types express program invariants and thereby provide valuable information for program optimization and debugging. A soft typecheckeruses the types inferred by a soft type system to eliminate run-time checks that are provably unnecessary; any remaining run-time checks are flagged as potential program errors.Soft Schemeis a practical soft type checker for R4RS Scheme. Its underlying type system generalizes conventional Hindley-Milner type inference by incorporating recursive types and a limited form of union type. Soft Scheme accommodates all of R4RS Scheme including uncurried procedures of fixed and variable arity, assignment, and continuations.

ion Robert Cartwright Matthias Felleisen Department of Computer Science Rice University Houston, TX 77251-1892 Rice Technical Report CS 91-167 A preliminary version of this technical report appeared in the Proceedings of the 19th Annual ACM Symposium on Principles of Programming Languages, January 19--22, 1992, Albuquerque, New Mexico. Copyright c fl1992 by Robert Cartwright and Matthias Felleisen 1 Full Abstraction and Sequentiality 1 1.1 Summary of Previous Work : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 1.2 Summary of Results : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 2 PCF 4 2.1 Formal Semantics : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5 2.2 Observational Equivalence, Sequentiality : : : : : : : : : : : : : : : : : : : : 8 3 Observing Sequentiality 9 3.1 Using errors, programmers can observe the order of evaluation. : : : : : : : 10 3.2 Using control operators, programs can observe the order of evaluation. : : : 10...

of programs than ML.We have also developed an algorithm for frugally inserting run-time checks in programs that do not type check.

Optimizing and parallelizing compilers for procedural languages rely on various forms of program dependence graphs (pdgs) to express the essential control and data dependencies among atomic program operations. In this paper, we provide a semantic justification for this practice by deriving two different forms of program dependence graph — the output pdg and the def-order pdg—and their semantic definitions from non-strict generalizations of the denotational semantics of the programming language. In the process, we demonstrate that both the output pdg and the def-order pdg (with minor technical modifications) are conventional data-flow programs. In addition, we show that the semantics of the def-order pdg dominates the semantics of the output pdg and that both of these semantics dominate—rather than preserve—the semantics of sequential execution.

Denotational semantics is founded on a theory of higher order computation called domain theory, which formalizes a computation as a potentially infinite enumeration of finite elements that approximate the answer with progressively higher accuracy. Although existing formulations of domain theory provide an elegant framework for defining the abstract meaning of programs, these definitions are not effective because they fail to specify when computations terminate. A formulation of domain theory is presented that gives a natural topological characterization of termination: the evaluation of a program expression should terminate if and only if the expression denotes an element that is finite and maximal.>

To accommodate polymorphic data types and operations, several computer scientists--most notably MacQueen, Plotkin, and Sethi--have proposed formalizing types as ideals. Although this approach is intuitively appealing, the resulting type system is both complex and restrictive because the type constructor that creates function types is not monotonic, and hence not computable. As a result, types cannot be treated as data values, precluding the formalization of type constructors and polymorphic program modules (where types are values) as higher order computable functions. Moreover, recursive definitions of new types do not necessarily have solutions.

Despite the reputed limitations of first order logic, it is easy to state and prove almost all interesting properties of recursive programs within a simple first order theory, by using an approach we call “first order programming logic”. Unlike higher order logics based on fixed-point induction, first order programming logic is founded on deductive principles that are familiar to most programmers. Informal structural induction arguments (such as termination proofs for LISP append, McCarthy’s 91-function, and Ackermann’s function) have direct formalizations within the system. The essential elements of first order programming logic are: (1) The data domain D must be a finitely generated set that explicitly includes the “undefined” object $ \bot $ (representing nontermination) as well as ordinary data objects. (2) Recursive programs over D are treated as logical definitions augmenting a first order theory ofthe data domain. (3) The interpretation of a recursive program is the least fixed-point of the functional corresponding to the program. Since the data domain D is a finitely generated set, the first order axiomatization of D includes a structural induction axiom scheme. This axiom scheme serves as the fundamental “proof rule” of first order program-ming logic. The major limitation of first order programming logic is that every fixed-point of the functional corresponding to a recursive program is an acceptable interpretation for the program. The logic fails to capture the notion of least fixed-point. To overcome this limitation, we present a simple, effective procedure for transforming an arbitrary recursive program into an equivalent recursive program that has a unique fixed-point, yet retains the logical structure of the original. Given this transformation technique, it is our experience that first order programming logic is sufficiently powerful to prove almost any property of practical interest about the functions computed by recursive programs.

This paper proposes a practical alternative to program verification -- called formal program testing -- with similar, but less ambitious goals. Like a program verifier, a formal testing system takes a program annotated with formal specifications as input, generates the corresponding verification conditions, and passes them through a simplifier. After the simplification step, however, a formal testing system simply evaluates the verification conditions on a representative set of test data instead of trying to prove them. Formal testing provides strong evidence that a program is correct, but does not guarantee it. The strength of the evidence depends on the adequacy of the test data.

This paper introduces the path, a new programming language construct designed to supplant the use of pointers to access and destructively update recursive data structures. In contrast to the complex semantics and proof rules for pointers, the semantics and proof rules for paths are simple and abstract. In fact, they are easily formalized within a first-order theory of recursive data objects analogous to first-order number theory. We present a number of sample programs, including implementations of queues and binary trees, utilizing the new construct and prove that they are correct.

First Order Programming Logic is a simple, yet powerful formal system for reasoning about recursive programs. In its simplest form, it has one major limitation: it cannot establish any property of the least fixed point of a recursive program which is false for some other fixed point. To rectify this weakness, we present two intuitively distinct approaches to strengthening First Order Programming Logic and prove that either extension makes the logic relatively complete. In the process, we prove that the two approaches are formally equivalent. The relative completeness of the extended logic is significant because it suggests it can establish all "ordinary" properties (obviously we cannot escape the Godelian incompleteness inherent in any programming logic) of recursive programs including those which compute partial functions.The second contribution of this paper is to establish that First Order Programming Logic is applicable to iterative programs as well. In particular, we show that the intermittent assertions method--an informal proof method for iterative programs which has not been formalized--is conveniently formalized simply as sugared First Order Programming Logic applied to the recursive translations of iterative programs.

This paper presents a new version of Hoare's logic including generalized procedure call and assignment rules which correctly handle aliased variables. Formal justifications are given for the new rules.