Backward compatibility is the property that an old version of a library can safely be replaced by a new version without breaking existing clients. Formal reasoning about backward compatibility requires an adequate semantic model to compare the behavior of two library implementations. In the object-oriented setting with inheritance and callbacks, such a model must account for the complex interface between library implementations and clients.In this paper, we develop a fully abstract trace-based semantics for class libraries in object-oriented languages, in particular for Java-like sealed packages. Our approach enhances a standard operational semantics such that the change of control between the library and the client context is made explicit in terms of interaction labels. By using traces over these labels, we abstract from the data representation in the heap, support class hiding, and provide fully abstract package denotations. Soundness and completeness of the trace semantics is proven using specialized simulation relations on the enhanced operational semantics. The simulation relations also provide a proof method for reasoning about backward compatibility. (C) 2013 Elsevier B.V. All rights reserved.

In distributed object-oriented systems, objects belong to different locations. For example, in Java Remote Method Invocation (RMI), objects can be distributed over different Java virtual machines. Accessing a reference in RMI has crucially different semantics depending on whether the referred object is local or remote. Nevertheless, such references are not statically distinguished by the Java type system. This chapter presents location types, which statically distinguish far from near references. We present a formal type system for a minimal core language and develop a type inference system that gives maximally precise solutions satisfying further desirable properties. We prove soundness of the type system as well as soundness and correctness of the inference system. We have implemented location types as a pluggable type system for the ABS language, an object-oriented language with a concurrency and distribution model based on concurrent object groups. To facilitate programming with location types, we provide a tight integration of the type and inference system with an Eclipse-based integrated development environment (IDE) that presents inference results as overlays to the source code. The IDE drastically reduces the annotation overhead while providing full static type information to the programmer.

Maintenance and evolution of software systems require to modify or exchange system components. In many cases, we would like the new component versions to be backward compatible to the old ones, at least for the use in the given context. Whereas on the program level formal techniques to precisely define and verify backward compatibility are under development, the situation on the system level is less mature. A system component C has not only communication interfaces to other system components, but also to human users or the environment of the system. In such scenarios, compatibility checking of different versions of C needs more than program analysis: We suggest to use behavioral software models for compatibility checking. In our approach, the underlying system, the old and new component, and the nondeterministic behavior of the environment are modeled with the concurrent object-oriented behavioral modeling language ABS. Abstracting from implementation details, the checking becomes simpler than on the program level.

Large object-oriented software systems are usually structured using modules or packages to enable large-scale development using clean interfaces that promote encapsulation and information hiding. However, in most OO languages, package interfaces (or signatures) are only implicitly defined. In this paper, we propose explicit package signatures that allow for modularly type-checking packages. We show how the signatures can be derived from packages and define a checkable specialization relation for package signatures. As main contribution, we show that if the package signatures of a new component version C new specialize the signatures of the old version C old , then C new type-checks in all contexts in which C old type-checks. That is, we extend checking of interface types to the level of packages.

Proving that a library implementation is backward compatible with an older version can be challenging, as the internal representation of the library might completely change and the clients of the library are usually unknown. This is particularly difficult in the setting of object-oriented programs with complex heaps and callbacks. Mechanical verification is a key success factor to make such proofs feasible. In this paper, we present a technique to verify backward compatibility or equivalence of class libraries. The technique works for complex implementations, with recursion and loops, in the setting of unknown program contexts. Reasoning about backward compatibility is done in terms of a special simulation relation between programs that use the old library implementation and programs that use the new library implementation. The verification process relies on a coupling invariant that describes this relation. We introduce a novel specification language to formulate coupling invariants and present the BCVERIFIER tool, first of its kind, that implements the verification approach using the automatic verifier BOOGIE. Our approach is validated by a number of classic examples.

Proving that a library is backwards compatible to an older version can be challenging, as the internal representation of the libraries might completely differ and the clients of the library are usually unknown. This is especially difficult in the setting of object-oriented programs with complex heaps and callbacks. Mechanical verification is a key success factor to make such proofs practicable. In this paper, we present a technique to verify the backwards compatibility or equivalence of class libraries in the setting of unknown program contexts. For a number of textbook examples we have formulated the verification conditions as input to the Boogie program verification system and validated the approach.

In distributed object-oriented systems, objects belong to different locations. For example, in Java RMI, objects can be distributed over different JVM instances. Accessing a reference in RMI has crucial different semantics depending on whether the referred object is local or remote. Nevertheless, such references are not statically distinguished by the type system. This paper presents location types, which statically distinguish far from near references. We present a formal type system for a minimal core language. In addition, we present a type inference system that gives optimal solutions. We implemented location types as a pluggable type system for the ABS language, an object-oriented language with a concurrency model based on concurrent object groups. An important contribution of this paper is the combination of the type system with the flexible inference system and a novel integration into an Eclipse-based IDE by presenting the inference results as overlays. This drastically reduces the annotation overhead while providing full static type information to the user. The IDE integration is a general approach of its own and can be applied to many other type system extensions.

We develop a fully abstract trace-based semantics for sets of classes in object-oriented languages, in particular for Java-like sealed packages. Our approach enhances a standard operational semantics such that the change of control between the package and the client context is made explicit in terms of interaction labels. By using traces over these labels, we abstract from the data representation in the heap, support class hiding, and provide fully abstract package denotations. The soundness and completeness of our approach is proven using innovative simulation techniques.

Software libraries and platforms should often evolve in a way that existing client code is not affected. As a prerequisite, client code that compiles against the original version of the libraries should also compile against the modified version. In such a case, we call the new version source compatible with the old one. For languages with elaborate static encapsulation mechanisms like Java, source compatibility is a complex property and checking tools do not exist. This paper defines source compatibility for packages of a formalized Java subset with all relevant access modifiers. As the definition quantifies over all possible client contexts, it cannot be used for automatic checking. We thus derive statically checkable conditions for compatibility that are proved necessary and sufficient. Such checkable conditions give interesting insight into the encapsulation of Java packages, allow to discuss language and program design aspects and provide the basis for package-local refactoring tools.

The literature distinguishes between trace-based and statebased specification techniques for object-oriented components. Tracebased specifications describe behavior in terms of the message histories of components, while state-based techniques explain component behavior in terms of states. The latter define how the state is changed by method calls and what is returned as a result. The state space is either abstract or concrete. Abstract states are used to model the behavior without referring to the implementation. Concrete states are expressed by the underlying implementation. State-based specifications are usually described in terms of preand postconditions of methods. In this paper, we investigate the relationship between trace-based specifications and specifications based on abstract states for sequential, objectbased components. We first generalize state-based techniques so that they can handle callbacks. Then, we develop formal models for tracebased and state-based specifications and show that every trace-based model can be canonically represented as a state-based model. Adapting notions from process simulation, we define an abstraction relation between two state-based models allowing their comparison. In particular, state-based models are more abstract than trace-based models. We also show that there exist most abstract models. The developed framework is illustrated by a subject component of the Subject-Observer Pattern.

Formal specification and verification techniques for object-oriented programs have evolved tremendously in the last ten years. However a big short-coming of existing approaches is that most object-oriented languages have no clear notion of component, or if they have, this notion doesn’t fit very well with existing programming practices. Hence, there also is a lack for specification techniques at the program component level. In this thesis, our components are the ones defined by Poetzsch-Heffter, Gaillourdet and Schäfer. They define their program components as dynamic entities which consist of a varying set of objects, and their boundary to the environment. Component behaviours are defined as partial functions from incoming to outgoing messages. Starting from this notion of component behaviour, we build our specification technique. We define a formal framework for integrating specification languages for components, and give one concrete instance of such a specification language, which is a mixture of a declarative and operational one. We then map the formal concepts to the Java programming language, describe the resulting issues, our concrete implementation and the underlying design decisions. Finally we develop a framework for checking the specifications at runtime.

The example of use which was chosen as the Common Component Modeling Example (CoCoME) and on which the several methods presented in this book should be applied was designed according to the example described by Larman in [1]. The description of this example and its use cases in the current chapter shall be considered under the assumption that this information was delivered by a business company as it could be in the reality. Therefore the specified requirements are potentially incomplete or imprecise.

We present a formal specification technique for object-oriented program components based on their boundary message behaviour. Component specifications describe restrictions on the set of message traces for a component without referring to actual implementations. Finally, we provide a framework to link specifications with abstract states to their implementations.

Finding good abstractions to model and express partial update , mobility and wrapping in object-oriented systems remains challenging. In this paper, we propose Comp, a process calculus approach for component models that merges aspects of object-orientation and evolution . The key features of Comp are: a hierarchical structure of components; the capacity to move, update, wrap components; method interfaces for components; and some isolation capacities to encode distribution and wrapping. Specifically, we introduce the syntax of Comp and formulate its operational semantics. We show a number of examples of use of Comp, with particular emphasis on common evolution patterns for components.

This paper describes a specification and verification tech- nique for object-oriented programs with invariants, known as the Boogie approach. The approach is proved to allow sound and modular verifi- cation. Topics covered by this paper are object hierarchies, subclassing, and advanced routine specifications. It also includes a discussion about the concrete implementation of these concepts in Spec# .