Wednesday, 23 June
  8:00 - 9:00 Registration
  9:00 - 9:30 Welcome
  9:30 - 10:30 Keynote:
Code Roots - Doug Lea
  10:30 - 11:00 Coffee break
  11:00 - 12:30 Session I:
Programming environments and tools
  12:30 - 14:00 Lunch
  14:00 - 15:30 Session II:
Theoretical foundations of programming languages
  15:30 - 16:00 Coffee break
  16:00 - 17:30 Session III:
Formal methods


Thursday, 24 June
  9:00 - 10:30 Keynote:
The role of empirical methods in software practice - David Budgen
  10:30 - 11:00 Coffee break
  11:00 - 12:30 Session IV:
Concurrency models in Java
  12:30 - 14:00 Lunch
  14:00 - 15:30 Panel:
The role of empirical methods in software practice
Special session:
Empirical methods
  15:30 - 16:00 Coffee break
  16:00 - 17:30 Session V:
Type systems


Friday, 25 June
  9:30 - 10:30 Keynote:
Secret Valley - Erik Ernst
  10:30 - 11:00 Coffee break
  11:00 - 12:30 Session VI:
Language design and implementation
  12:30 - 14:00 Lunch
  14:00 - 15:30 Session VII:
Concurrency abstractions
  15:30 - 16:00 Coffee break
  16:00 - 17:30 Session VIII:
Experiences


KEYNOTES


Code Roots
chair: Eric Jul

Doug Lea - Computer Science Department, State University of New York at Oswego, USA

This talk uses snippets of code to illustrate the interplay of ideas and engineering behind object-oriented libraries. Examples include those showing the influences of ECOOP papers, bug reports, and standards bodies; and conversely, those showing how new APIs impact developers and researchers.

The role of empirical methods in software practice
chair: Theo D’Hondt

David Budgen

Empirical studies have been used for evaluating software engineering practices, concepts, and products since the 1970s, with a significant growth in activity over the past two decades. However, the current state of the discipline is that practice, standards, curricula and policies are still heavily dependent upon expert opinion (at best) and sometimes simply upon what is little more than advocacy. A good example of this use of expert opinion is the Software Engineering Body of Knowledge (SWEBOK): this is often quoted as an authoritative source, yet it is one that contains relatively few references to empirical studies.
While expert judgement does have value, especially in the absence of more rigorous forms of data, it does not (and cannot) provide a sound basis for the evolution of an engineering culture. This weakness, reflected in the way that we perform our research, was highlighted through a series of reviews of research studies conducted by Bob Glass and co-workers in the early 2000s, with their findings providing some degree of quantification of the shortcomings in our discipline’s research profile.
The adoption of the evidence-based paradigm since 2004, derived from the experiences of clinical medicine and other disciplines, has now provided software engineering with a framework within which it is possible to position empirical studies to much greater effect. Its use of secondary studies, such as systematic literature reviews, for aggregating empirical knowledge, as well as for identifying where such knowledge is lacking, is beginning to provide a valuable ‘evidence map’ of our discipline. This in turn is encouraging researchers both to perform more empirical studies, as well as to employ a wider range of forms for conducting them.
My presentation will examine these issues and discuss the implications for software engineering in general—as well as for the object-oriented paradigm in particular.

Secret Valley
chair: Eric Jul

Erik Ernst - Dept. of Computer Science, Aarhus University, Denmark

This talk takes a look at object-oriented programming language design from a location outside the mainstream, namely the Scandinavian tradition going from the first object-oriented language SIMULA, through Beta which takes unification to an extreme, to gbeta which generalizes Beta in many ways. A range of underlying issues are considered, including the relation to the structure of human thinking and natural language, the dynamic semantics of the language, and the static analysis supported by its type system.
The developments in this secret valley of programming language design did actually give rise to a small mountain stream of ideas that flowed out of the valley and into the main stream in various ways over the years. We hope to illustrate that the exploration of such a somewhat esoteric position in the language design space may give rise to some fresh ideas for the rest of the world to think about now and then.
 

PAPER ABSTRACTS


Session I
chair: Shigeru Chiba

Detecting Missing Method Calls in Object-Oriented Software

  • Martin Monperrus - TU Darmstadt, Germany
  • Marcel Bruch - TU Darmstadt, Germany
  • Mira Mezini - TU Darmstadt, Germany

When using object-oriented frameworks it is easy to overlook certain important method calls that are required at particular places in code. In this paper, we provide a comprehensive set of empirical facts on this problem, starting from traces of missing method calls in a bug repository. We propose a new system, which automatically detects them during both software development and quality assurance phases.
The evaluation shows that it has a low false positive rate (<5%) and that it is able to find missing method calls in the source code of the Eclipse IDE.

Debugging Model-Transformation Failures Using Dynamic Tainting

  • Pankaj Dhoolia - IBM Research - India, India
  • Senthil Mani - IBM Research - India, India
  • Vibha Singhal Sinha - IBM Research - India, India
  • Saurabh Sinha - IBM Research - India, India

Model-to-text (M2T) transforms are a class of software applications that translate a structured input into text output. The input models to such transforms are complex, and faults in the models that cause an M2T transform to generate an incorrect or incomplete output can be hard to debug. We present an approach based on dynamic tainting to assist transform users in debugging input models. The approach instruments the transform code to associate taint marks with the input-model elements, and propagate the marks to the output text. The taint marks identify the input-model elements that either contribute to an output string, or cause potentially incorrect paths to be executed through the transform, which results in an incorrect or a missing string in the output. We implemented our approach for XSL-based transforms and conducted empirical studies. Our results illustrate that the approach can significantly reduce the fault search space and, in many cases, precisely identify the input-model faults. The main benefit of our approach is that it automates, with a high degree of accuracy, a debugging task that can be tedious to perform manually.

Automatically Extracting Class Diagrams from Spreadsheets

  • Felienne Hermans - Delft University of Technology, Netherlands
  • Martin Pinzger - Delft University of Technology, Netherlands
  • Arie van Deursen - Delft University of Technology, Netherlands

The use of spreadsheets to capture information is widespread in industry. Spreadsheets can thus be a wealthy source of domain information. We propose to automatically extract this information and transform it into class diagrams. The resulting class diagram can be used by software engineers to understand, refine, or re-implement the spreadsheet's functionality. To enable the transformation into class diagrams we create a library of common spreadsheet usage patterns. These patterns are localized in the spreadsheet using a two- dimensional parsing algorithm. The resulting parse tree is transformed and enriched with information from the library. We evaluate our approach on the spreadsheets from the Euses Spreadsheet Corpus by comparing a subset of the generated class diagrams with reference class diagrams created manually.
 

Session II
chair: Mira Mezini

Adding Dynamic Types to C#

  • Gavin M. Bierman - Microsoft Research, United Kingdom
  • Erik Meijer - Microsoft Corporation, United States
  • Mads Torgersen - Microsoft Corporation, United States

Developers using statically typed languages such as C# and Java are increasingly having to interoperate with APIs and object models defined in dynamic languages. This impedance mismatch results in code that is difficult to understand, awkward to analyze, and expensive to maintain. In this paper we describe new features in C# 4.0 that support the safe combination of dynamically and statically typed code by deferring type checking of program fragments with static type dynamic until runtime. When executed, these dynamic code fragments are type-checked and resolved using the same rules as statically typed code. We formalize these features in a core fragment of C# and prove important safety properties. In particular, we show that subtyping remains transitive.

Essential AOP: The A Calculus

  • Bruno De Fraine - Software Languages Lab, Vrije Universiteit Brussel, Belgium
  • Erik Ernst - Department of Computer Science, Aarhus University, Denmark
  • Mario Südholt - Département Informatique, École des Mines de Nantes, France

Aspect-oriented programming (AOP) has produced interesting language designs, but also ad-hoc semantics that needs clarification. We contribute to this clarification with a calculus that models essential AOP, both simpler and more general than existing formalizations. In AOP, advice may intercept method invocations, and proceed executes the suspended call. Proceed is an ad-hoc mechanism, only usable inside advice bodies. Many pointcut mechanisms, e.g. wildcards, also lack regularity. We model proceed using first-class closures, and shift complexity from pointcuts to ordinary object-oriented code. Two well-known pointcut categories, call and execution, are commonly considered similar. We formally expose their differences, and resolve the associated soundness problem. Our calculus includes type ranges, an intuitive and concise alternative to explicit type variables that allows advice to be polymorphic over intercepted methods. We use calculus parameters to cover type safety for a wide design space of other features. Type soundness is verified in Coq.

The Essence of JavaScript

  • Arjun Guha - Brown University, United States
  • Claudiu Saftoiu - Brown University, United States
  • Shriram Krishnamurthi - Brown University, United States

We reduce JavaScript to a core calculus structured as a small-step operational semantics. We present several peculiarities of the language and show that our calculus models them. We explicate the desugaring process that turns JavaScript programs into ones in the core. We demonstrate faithfulness to JavaScript using real-world test suites. Finally, we illustrate utility by defining a security property, implementing it as a type system on the core, and extending it to the full language.
 

Session III
chair: Frank Piessens

Verifying Executable Object-Oriented Specifications with Separation Logic

  • Stephan Staden - ETH Zurich, Switzerland
  • Cristiano Calcagno - Monoidics Ltd and Imperial College, London, United Kingdom
  • Bertrand Meyer - ETH Zurich, Switzerland

Specifications of Object-Oriented programs conventionally employ Boolean expressions of the programming language for assertions. Programming errors can be discovered by checking at runtime whether an assertion, such as a precondition or class invariant, holds. In this work, we show how separation logic can be used to verify that these executable specifications will always hold at runtime. Both the program and its executable assertions are verified with respect to separation logic specifications. A novel notion called relative purity embraces historically problematic side-effects in executable specifications, and verification boils down to proving connecting implications. Even model-based specifications can be verified. The framework is also well-suited to separation logic proof tools and now implemented in jStar. Numerous automatically verified examples illustrate the framework's use and utility.

Verifying Generics and Delegates

  • Kasper Svendsen - IT University of Copenhagen, Denmark
  • Lars Birkedal - IT University of Copenhagen, Denmark
  • Matthew Parkinson - University of Cambridge, United Kingdom

Recently, object-oriented languages, such as C#, have been extended with language features prevalent in most functional languages: parametric polymorphism and higher-order functions. In the OO world these are called generics and delegates, respectively. These features allow for greater code reuse and reduce the possibilities for runtime errors. However, the combination of these features pushes the language beyond current object-oriented verification techniques.
In this paper, we address this by extending a higher-order separation logic with new assertions for reasoning about delegates and variables. We faithfully capture the semantics of C# delegates including their capture of the l-value of a variable, and that “stack” variables can live beyond their “scope”. We demonstrate that our logic is sound and illustrate its use by specifying and verifying a series of interesting and challenging examples.

Recency Types for Analyzing Scripting Languages

  • Phillip Heidegger - Albert-Ludwigs-Universität Freiburg, Germany
  • Peter Thiemann - Albert-Ludwigs-Universität Freiburg, Germany

Large programs are being built with dynamically typed languages. As these programs grow, semantics-based tools gain importance for detecting programming errors and for program understanding. As a basis for such tools, we propose a type system for a calculus that models essential features of JavaScript, a widely used dynamically-typed language: first-class functions, objects asproperty maps, and prototypes. Our type system infers precise singleton object types for recently allocated objects, which are handled flow-sensitively and change during the objects' initialization phase. Recency provides an automatic criterion to subsume precise object types to flow-insensitive summary object types. Thus, the type system identifies an initialization phase for each object during which the change of its value is precisely reflected in its type. Unlike linear types, summary types may refer to singleton types and vice versa. We prove the soundness of the type system and present and implement constraint-based inference algorithm.
 

Session IV
chair: Doug Lea

Correct Refactoring of Concurrent Java Code

  • Max Schaefer - Oxford University Computing Laboratory, United Kingdom
  • Julian Dolby - IBM T.J. Watson Research Center, United States
  • Manu Sridharan - IBM T.J. Watson Research Center, United States
  • Emina Torlak - IBM T.J. Watson Research Center, United States
  • Frank Tip - IBM T.J. Watson Research Center, United States

Automated refactorings as implemented in modern IDEs for Java usually make no special provisions for concurrent code.
Thus, refactored programs may exhibit unexpected new concurrent behaviors.
We analyze the types of such behavioral changes caused by current refactoring engines and develop techniques to make them behavior-preserving, ranging from simple techniques to deal with concurrency-related language constructs to a framework that computes and tracks synchronization dependencies.
By basing our development directly on the Java Memory Model, we can state and prove precise correctness results about refactoring concurrent programs.
We show that a broad range of refactorings are not influenced by concurrency at all, whereas other important refactorings can be made behavior-preserving for correctly synchronized programs by using our framework.
Experience with a prototype implementation shows that our techniques are easy to implement and require only minimal changes to existing refactoring engines.

Programming Coordinated Behavior in Java

  • David Harel - Weizmann Institute of Science, Rehovot, Israel, Israel
  • Assaf Marron - Weizmann Institute of Science, Rehovot, Israel, Israel
  • Gera Weiss - Ben Gurion University, Beer-Sheva, Israel, Israel

Following the scenario-based approach to programming which centered around live sequence charts (LSCs), we propose a general approach to software development in Java. A program will consist of modules called behavior threads (b-threads), each of which independently describes a scenario that may cross object boundaries. We identify a protocol and a coordination mechanism that allow such behavioral programming. Essentially, runs of programs are sequences of events that result from three kinds of b-thread actions: requesting that events be considered for triggering, waiting for triggered events, and blocking events requested by other b-threads. The coordination mechanism synchronizes and interlaces b-threads execution yielding composite, integrated system behavior. The protocol idioms and the coordination mechanism of b-threads are implemented as a Java library called BPJ. Throughout the exposition we illustrate benefits of the approach and discuss the merits of behavioral programming as a broad, implementation-independent paradigm.

JCoBox: Generalizing Active Objects to Concurrent Components

  • Jan Schäfer - University of Kaiserslautern, Germany
  • Arnd Poetzsch-Heffter - University of Kaiserslautern, Germany

Concurrency in object-oriented languages is still waiting for a satisfactory solution. For many application areas, standard mechanisms like threads and locks are too low level and have shown to be error-prone and not modular enough. Lately the actor paradigm has regained attention as a possible solution to concurrency in OOLs.
We propose JCoBox: a Java extension with an actor-like concurrency model based on the notion of concurrently running object groups, so-called coboxes. Communication is based on asynchronous method calls with standard objects as targets. Cooperative multi-tasking within coboxes allows for combining active and reactive behavior in a simple and safe way. Futures and promises lead to a data-driven synchronization of tasks.
This paper describes the concurrency model, the formal semantics, and the implementation of JCoBox, and shows that the performance of the implementation is comparable to state-of-the-art actor-based language implementations for the JVM.
 

Panel: Research for Programming Languages
Panelists: Awais Rashid (Chair), James Noble, Jan Vitek, David Budgen, Phil Greenwood

Ever wondered, what would be the best way to evaluate a new programming language or features of existing programming languages and systems? What makes a good empirical study? How does one design such a study, analyse the threats to validity and interpret the data resulting from the study? What key characteristics experts look out for when reviewing such research? This panel will be kicked off by a short presentation from Stefan Hannenberg with a study of the effect of type systems on programming tasks. This will be followed by a discussion of why such studies are challenging, what kind of challenges need to be overcome and what kind of methodological risks are there. The panel will then discuss how, as a community, we can encourage more active research on empirical studies of programming languages given the afore-mentioned challenges and risks. There will be ample time for the audience to participate in the discussion at the end.
 

Special session on empirical methods
chair: Awais Rashid

Doubts about the Positive Impact of Static Type Systems on Programming Tasks in Single Developer Projects - An Empirical Study

Stefan Hanenberg - University of Duisburg-Essen, Germany

Static type systems are one of the major topics in research, teaching, as well as in industry. However, while type systems are well-studied from a theoretical perspective, there is hardly any knowledge about the impact of static type systems on practical programming with a programming language. In literature, several arguments advocate the use of static type systems; at the same time, there are arguments which advocate the use of dynamic type systems: it is unclear which arguments describe observable phenomena and which do not. Here, empirical methods could help. It turns out, though, that the impact of static type systems is rarely studied using empirical methods. Following the research method of empirical software engineering, this paper introduces an experiment that studies the impact of static type systems.
 

Session V
chair: Mario Südholt

A Type System for Data-Centric Synchronization

  • Mandana Vaziri - IBM T.J. Watson Research Center, United States
  • Frank Tip - IBM T.J. Watson Research Center, United States
  • Julian Dolby - IBM T.J. Watson Research Center, United States
  • Christian Hammer - Purdue University, United States
  • Jan Vitek - Purdue University, United States

Data-centric synchronization groups fields of objects into atomic sets to indicate they must be updated atomically. Each atomic set has associated units of work, code fragments that preserve the consistency of that atomic set. We present a type system for data-centric synchronization that enables separate compilation and supports atomic sets that span multiple objects, thus allowing recursive data structures to be updated atomically. The type system supports full encapsulation for more efficient code generation. We evaluate our proposal using AJ, which extends the Java programming language with data-centric synchronization. We report on the implementation of a compiler and on refactoring classes from standard libraries and a multi-threaded benchmark to use atomic sets. Our results suggest that data-centric synchronization enjoys low annotation overhead while preventing high-level data races.

Type-Safe Eventful Sessions in Java

  • Raymond Hu - Imperial College London, United Kingdom
  • Dimitrios Kouzapas - Imperial College London, United Kingdom
  • Olivier Pernet - Imperial College London, United Kingdom
  • Nobuko Yoshida - Imperial College London, United Kingdom
  • Kohei Honda - Queen Mary, University of London, United Kingdom

Event-driven programming is a major paradigm in concurrent and communication-based programming, and a widely adopted approach to building scalable high-concurrency servers. However, traditional event-driven programs are more difficult to read, write and verify than their multi-threaded counterparts due to low-level APIs and fragmentation of control flow across disjoint event handlers.
This paper presents a Java language extension and a novel type discipline for type-safe event-driven session programming that counters the problems of traditional event-based programming with abstractions and safety guarantees based on session types, while retaining the expressiveness and performance characteristics of events. The type discipline extends session types and their primitives with asynchronous input, session typecase and session set types, ensuring event-handling safety and event progress in addition to the standard type soundness and communication safety. The advantages, expressiveness and performance of event-driven session programming are demonstrated through a range of examples and benchmarks, including a session-typed SMTP server.

Capabilities for Uniqueness and Borrowing

  • Philipp Haller - EPFL, Switzerland, Switzerland
  • Martin Odersky - EPFL, Switzerland, Switzerland

An important application of unique object references is safe and efficient message passing in concurrent object-oriented programming. However, to prevent the ill effects of aliasing, practical systems often severely restrict the shape of messages passed by reference. Moreover, the problems of destructive reads are exacerbated in a concurrent setting.
This paper introduces a new approach to uniqueness. The idea is to use capabilities for enforcing both at-most-once consumption of unique references, and a flexible notion of uniqueness. The main novelty of our approach is a model of uniqueness and borrowing based on simple, unstructured capabilities, thereby providing simple foundations. We formalize our approach using a relatively simple type system, for which we provide a complete soundness proof. We have implemented our type system as an extension to Scala. Practical experience suggests that our system allows type checking real-world actor-based concurrent programs with only a small increase in type annotations.
 

Session VI
chair: Erik Ernst

Embedding Languages Without Breaking Tools

  • Lukas Renggli - Software Composition Group, University of Bern, Switzerland, Switzerland
  • Tudor Gîrba - Software Composition Group, University of Bern, Switzerland, Switzerland
  • Oscar Nierstrasz - Software Composition Group, University of Bern, Switzerland, Switzerland

Domain-specific languages (DSLs) are increasingly used as embedded languages within general-purpose host languages. DSLs provide a compact, dedicated syntax for specifying parts of an application related to specialized domains. Unfortunately, such language extensions typically do not integrate well with the development tools of the host language. Editors, compilers and debuggers are either unaware of the extensions, or must be adapted at a non-trivial cost. We present a novel approach to embed DSLs into an existing host language by leveraging the underlying representation of the host language used by these tools. Helvetia is an extensible system that intercepts the compilation pipeline of the Smalltalk host language to seamlessly integrate language extensions. We validate our approach by case studies that demonstrate three fundamentally different ways to extend or adapt the host language syntax and semantics.

Modules as Objects in Newspeak

  • Gilad Bracha - Ministry of Truth, United States
  • Peter von der Ahé - Ministry of Truth, Denmark
  • Vassili Bykov - Ministry of Truth, United States
  • Yaron Kashai - Cadence Design Systems, United States
  • William Maddox - Adobe Systems, United States
  • Eliot Miranda - Teleplace, United States

We describe support for modularity in Newspeak, a programming language descended from Smalltalk and Self. Like Self, all computation - even an object’s own access to its internal structure - is performed by invoking methods on objects. However, like Smalltalk, Newspeak is class-based. Classes can be nested arbitrarily, as in Beta. Since all names denote method invocations, all classes are virtual; in particular, superclasses are virtual, so all classes act as mixins. Unlike its predecessors, there is no static state in Newspeak, nor is there a global namespace. Modularity in Newspeak is based exclusively on class nesting. There are no separate modularity constructs such as packages. Top level classes act as module definitions, which are independent, immutable, self-contained parametric namespaces. They can be instantiated into modules which may be stateful and mutually recursive.

Inline Caching meets Quickening

Stefan Brunthaler - Institute of Computer Languages, Vienna University of Technology, Austria

Inline caches effectively eliminate the overhead implied by dynamic typing. Yet, inline caching is mostly used in code generated by just-in-time compilers. We present efficient implementation techniques for using inline caches without dynamic translation, thus enabling future interpreter implementers to use this important optimization technique-we report speedups of up to a factor of 1.71-without the additional implementation and maintenance costs incurred by using a just-in-time compiler.
 

Session VII
chair: Jan Vitek

Self-Replicating Objects for Multicore Platforms

Krzysztof Ostrowski - Cornell University, United States Chuck Sakoda - Cornell University, United States Ken Birman - Cornell University, United States
The paper introduces Self-Replicating Objects (SROs), a new concurrent programming abstraction. An SRO is implemented and used much like an ordinary .NET object and can expose arbitrary user-defined APIs, but it is aggressive about automatically exploiting multicore CPUs. It does so by spontaneously and transparently partitioning its state into a set of replicas that handle method calls in parallel and automatically merging replicas before processing calls that cannot execute in the replicated state. Developers need not be concerned about protecting access to shared data; each replica is a monitor and has its own state. The runtime ensures proper synchronization, scheduling, decides when to split/merge, and can transparently migrate replicas to other processes to decrease contention. Compared to threads/locks or toolkits such as .NET Parallel Extensions, SROs offer a simpler, more versatile programming model while delivering comparable, and in some cases even higher performance.

Reasoning about the Implementation of Concurrency Abstractions on x86-TSO

Scott Owens - University of Cambridge, United Kingdom
With the rise of multi-core processors, shared-memory concurrency has become a widespread feature of computation, from hardware, to operating systems, to programming languages such as C++ and Java. However, none of these provide sequentially consistent shared memory; instead they have relaxed memory models, which make concurrent programs even more challenging to understand. Programming language implementations run on hardware memory models, so VM and run-time system implementors must reason at both levels. Of particular interest are the low-level implementations of the abstractions that support language-level concurrency-especially because they invariably contain data races. In this paper, we develop a novel principle for reasoning about assembly programs on our previous x86-TSO memory model, and we use it to analyze five concurrency abstraction implementations: two spinlocks (from Linux); a non-blocking write protocol; the double-checked locking idiom; and java.util.concurrent's Parker. Our principle, called triangular-race freedom, strengthens the usual data-race freedom style of reasoning.

Concurrent Abstract Predicates

  • Thomas Dinsdale-Young - Imperial College, London, United Kingdom
  • Mike Dodds - University of Cambridge, United Kingdom
  • Philippa Gardner - Imperial College, London, United Kingdom
  • Matthew J Parkinson - University of Cambridge, United Kingdom
  • Viktor Vafeiadis - University of Cambridge, United Kingdom

Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a program logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module's implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.
 

Session VIII
chair: James Noble

The Use of Overloading in JAVA Programs

  • Joseph (Yossi) Gil - IBM Haifa Research Laboratory, Israel
  • Keren Lenz - Department of Computer Science, The Technion, Haifa, Israel

Method overloading is a controversial language feature, especially in the context of Object Oriented languages, where its interaction with overriding may lead to confusing semantics. One of the main arguments against overloading is that it can be abused by assigning the same identity to conceptually different methods.
This paper describes a study of the actual use of overloading in JAVA. To this end, we developed a taxonomy of classification of the use of overloading, and applied it to a large JAVA corpus comprising more than 100,000 user defined types. We found that more than 14% of the methods in the corpus are overloaded. Using sampling and evaluation by human raters we found that about 60% of overloaded methods follow one of the “non ad hoc use of overloading patterns” and that additional 20% can be easily rewritten in this form. The most common pattern is the use of overloading as an emulation of default arguments, a mechanism which does not exist in JAVA.

Falling Back on Executable Specifications

  • Hesam Samimi - University of California, Los Angeles, United States
  • Ei Darli Aung - University of California, Los Angeles, United States
  • Todd Millstein - University of California, Los Angeles, United States

We describe a new approach to employing specifications for software reliability. Rather than only using specifications to validate implementations, we additionally employ specifications as a reliable alternative to those implementations. Our approach, which we call Plan B, performs dynamic contract checking of methods. However, instead of halting the program upon a contract violation, we employ a constraint solver to automatically execute the specification in order to allow the program to continue properly. This paper describes Plan B as well as its instantiation in an extension to Java with executable specifications that we call PBnJ (Plan B in Java). We present the design of PBnJ by example and describe its implementation, which leverages the Kodkod relational constraint solver.
We also describe our experience using the language to enhance the reliability and functionality of several existing Java applications.

Contract-based Data Structure Repair Using Alloy

  • Razieh Nokhbeh Zaeem - The University of Texas at Austin, United States
  • Sarfraz Khurshid - The University of Texas at Austin, United States

Contracts and specifications have long been used in object-oriented design, programming and testing to enhance reliability before software deployment. However, the use of specifications in deployed software is commonly limited to runtime checking where assertions form a basis for detecting incorrect program states to terminate the erroneous executions. This paper presents a contract-based approach for data structure repair, which allows repairing erroneous executions in deployed software by repairing erroneous states. The key novelty is the support for rich behavioral specifications, such as those that relate pre-states with post-states of the method to accurately specify expected behavior and hence to enable precise repair. The approach is based on the view of a specification as a non-deterministic implementation, which may permit a high degree of non-determinism. The key insight is to use any correct state mutations by an otherwise erroneous execution to prune the non-determinism in the specification, thereby transmuting the specification to an implementation that does not incur a prohibitively high performance penalty. While invariants, pre-conditions and post-conditions could be provided in different modeling languages, we leverage the Alloy tool-set, specifically the Alloy language and the Alloy Analyzer for systematically repairing erroneous states. Four different algorithms are presented and implemented in our data structure repair framework. Experiments using complex specifications show the approach holds much promise in increasing software reliability.