In today’s complex software, internal trusted code is tightly intertwined with external untrusted code. To reason about internal code, programmers must reason about the potential effects of calls to external code, even though that code is not trusted and may not even be available. The effects of external calls can be limited if internal code is programmed defensively, limiting potential effects by limiting access to the capabilities necessary to cause those effects. This paper addresses the specification and verification of internal code that relies on encapsulation and object capabilities to limit the effects of external calls. We propose new assertions for access to capabilities, new specifications for limiting effects, and a Hoare logic to verify that a module satisfies its specification, even while making external calls. We illustrate the approach though a running example with mechanised proofs, and prove soundness of the Hoare logic.

Robust modules guarantee to do only what they are supposed to do – even in the presence of untrusted malicious clients, and considering not just the direct behaviour of individual methods, but also the emergent behaviour from calls to more than one method. Necessity is a language for specifying robustness, based on novel necessity operators capturing temporal implication, and a proof logic that derives explicit robustness specifications from functional specifications. Soundness and an exemplar proof are mechanised in Coq.

The vast gap between CPU and RAM speed means that on modern architectures, developers need to carefully consider data placement in memory to exploit spatial and temporal cache locality and use CPU caches effectively. To that extent, developers have devised various strategies regarding data placement; for objects that should be close in memory, a contiguous pool of objects is allocated and then new instances are constructed inside it; an array of objects is clustered into multiple arrays, each holding the values of a specific field of the objects. Such data placements, however, have to be performed manually, hence readability, maintainability, memory safety, and key OO concepts such as encapsulation and object identity need to be sacrificed and the business logic needs to be modified accordingly. We propose a language extension, SHAPES, which aims to offer developers high-level fine-grained control over data placement, whilst retaining memory safety and the look-and-feel of OO. SHAPES extends an OO language with the concepts of pools and layouts: Developers declare pools that contain objects of a specific type and specify the pool’s layout. A layout specifies how objects in a pool are laid out in memory. That is, it dictates how the values of the fields of the pool’s objects are grouped together into clusters. Objects stored in pools behave identically to ordinary, standalone objects; the type system allows the code to be oblivious to the layout being used. This means that the business logic is completely decoupled from any placement concerns and the developer need not deviate from the spirit of OO to better utilise the cache. In this paper, we present the features of SHAPES, as well as the design rationale behind each feature. We then showcase the merit of SHAPES through a sequence of case studies; we claim that, compared to the manual pooling and clustering of objects, we can observe improvement in readability and maintainability, and comparable (i.e., on par or better) performance. We also present SHAPES^h, an OO calculus which models the SHAPES ideas, we formalise the type system, and prove soundness. The SHAPES^h type system uses ideas from Ownership Types [Clarke et al., 2013] and Java Generics [Gosling et al., 2014]: In SHAPES^h, pools are part of the types; SHAPES^h class and type definitions are enriched with pool parameters. Moreover, class pool parameters are enriched with bounds, which is what allows the business logic of SHAPES to be oblivious to the layout being used. SHAPES^h types also enforce pool uniformity and homogeneity. A pool is uniform if it contains objects of the same class only; a pool is homogeneous if the corresponding fields of all its objects point to objects in the same pool. These properties allow for more efficient implementation. For performance considerations, we also designed SHAPES^l, an untyped, unsafe low-level language with no explicit support for objects or pools. We argue that it is possible to translate SHAPES^l into existing low-level intermediate representations, such as LLVM [Lattner and Adve, 2004], present the translation of SHAPES^h into SHAPES^l, and show its soundness. Thus, we expect SHAPES to offer developers more fine-grained control over data placement, without sacrificing memory safety or the OO look-and-feel.

Functional specifications describe what program components can do: the sufficient conditions to invoke components’ operations. They allow us to reason about the use of components in a closed world setting, where components interact with known client code, and where the client code must establish the appropriate pre-conditions before calling into a component. Sufficient conditions are not enough to reason about the use of components in an open world setting, where components interact with external code, possibly of unknown provenance, and where components may evolve over time. In this open world setting, we must also consider the necessary conditions, i. e. what are the conditions without which an effect will not happen. In this paper we propose the $${\mathcal {C}}$$ hainmail specification language for writing holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for $${\mathcal {C}}$$ hainmail, and discuss several examples. The core of $${\mathcal {C}}$$ hainmail has been mechanised in the Coq proof assistant.

Type family applications in Haskell must be fully saturated. This means that all type-level functions have to be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension to GHC that removes this restriction. We augment Haskell’s existing type arrow, |->|, with an unmatchable arrow, | >|, that supports partial application of type families without compromising soundness. A soundness proof is provided. We show how the techniques described can lead to substantial code-size reduction (circa 80%) in the type-level logic of commonly-used type-level libraries whilst simultaneously improving code quality and readability.

This paper presents a new lightweight technique for auto-matically generating high coverage test suites for Haskell library code. Our approach combines four main features to increase test coverage: (1) automatically inferring the constructors and functions needed to generate test data; (2) using needed narrowing to take advantage of Haskell’s lazy evaluation semantics; (3) inspecting elements inside re-turned data structures through the use of case statements, and (4) efficiently handling polymorphism by lazily instan-tiating all possible instances. We have implemented this technique in Irulan, a fully au-tomatic tool for systematic black-box unit testing of Haskell library code. We have designed Irulan to generate high cov-erage test suites and detect common programming errors in the process. We have applied Irulan to over 50 programs from the spectral and real suites of the nofib benchmark and show that it can effectively generate high-coverage test suites—exhibiting 70.83 % coverage for spectral and 59.78% coverage for real—and find errors in these programs. Our techniques are general enough to be useful for several other types of testing, and we also discuss our experience of using Irulan for property and regression testing.

The definitive version can be found at : http://onlinelibrary.wiley.com/ Copyright Wiley [Full text of this article is not available in the UHRA]

Even Haskell programs can occasionally go wrong.Programs calling head on an empty list, and incomplete patterns in function definitions can cause program crashes, reporting little more than the precise location where error was ultimately called.Being told that one application of the head function in your program went wrong, without knowing which use of head went wrong can be infuriating.We present our work on adding the ability to get stack traces out of GHC, for example that our crashing head was used during the evaluation of foo, which was called during the evaluation of bar , during the evaluation of main.We provide a transformation that converts GHC Core programs into ones that pass a stack around, and a stack library that ensures bounded heap usage despite the highly recursive nature of Haskell.We call our extension to GHC StackTrace.

The zipper is a well known design pattern for providing a cursor-like interface to a data structure. However, the classic treatise by Huet (1) only scratches the surface of some of the potential applications of the zipper. In this work we have taken inspiration from Huet, and built a library suitable as an underpinning for a structured editor for programming languages. We consider a zipper structure that is suitable for traversing heterogeneous data types, encoding routes to other places in the tree (for bookmark or quick-jump functionality), expressing lexically bound information using contexts, and traversals for rendering a program indicating where the cursor is currently focused in the whole.

As those who have done it can attest, developing an undergraduate degree in software engineering is a daunting and challenging task, and there have been instances where a department has tried, but failed to get its program approved. A strong desire to develop a program in software engineering together with interested faculty may not be enough to build a credible degree, let alone a curriculum that will be approved by all the administrative and State organizations who may have a say in it .This panel brings together a group whose experience in developing software engineering degrees at their respective institutions may be helpful to those thinking about doing so. Each member of the group will describe his/her experiences in developing an undergraduate program in software engineering and address key issues and problems that should be considered in any such effort. There will also be ample opportunity for interaction among the participants.

The distributed development and maintenance paradigm for component delivery is fraught with problems. One wants a relationship between developers and clients that is autonomous and anonymous. Yet components written in languages such as C++ require the recompilation of all dependent subsystems when a new version of a component is released. The design of Java's binary format has side-stepped this constraint, removing the need for total recompilation with each change. But the potential is not fulfilled if programs have to be stopped to swap in each new component. This paper describes a framework that allows Java programs to be dynamically upgraded. Its key purpose is to allow libraries that are safe to replace existing libraries without adversely affecting running programs. The framework provides developers with a mechanism to release their libraries and provides clients with the surety of only upgrading when it is safe to do so.

Abstract Configuration and coordination are central issues in the design and implementation of middleware systems and are one of the reasons why building such systems is more complex than constructing stand‐alone sequential programs. Through configuration, the structure of the system is established—which elements it contains, where they are located and how they are interconnected. Coordination is concerned with the interaction of the various components—when an interaction takes place, which parties are involved, what protocols are followed. Its purpose is to coordinate the behaviour of the various components to meet the overall system specification. The open and adaptive nature of middleware systems makes the task of configuration and coordination particularly challenging. We propose a model that can operate in such an environment and enables the dynamic integration and coordination of components by observing and coercing their behaviour through the interception of the messages exchanged between them. Copyright © 2003 John Wiley & Sons, Ltd.

The promises of object-orientation and distributed computing could be delivered if the software we needed were written in stone. But it isn't, it changes. The challenge of distributed object-oriented maintenance is to find a means of evolving software, which already has a distributed client base. Working within this scenario, we observe how certain object-oriented language systems seek to support differing client requirements and service obligations. In particular, we examine how the Java Language Specification (JLS) facilitates the concept of binary compatibility, a useful property, but one that may introduce a class of clients who dare not re-compile! Following a suggestion in the new draft JLS, we describe our tool to manage distributed version control and we formulate some proposals for future developments.

Formal techniques for Java programsFormal techniques can help analyze programs, precisely describe program behavior, and verify program properties.Applying such techniques to object-oriented technology is especially interesting because• the object-oriented (OO) paradigm forms the basis for the software component industry with their need for certification techniques, • it is widely used for distributed and network programming and • the potential for reuse in OO programming carries over to reusing specifications and proofs.Such formal techniques are sound, only if based on a formalization of the language itself.Java is a good platform to bridge the gap between formal techniques and practical program development.It plays an important role in these areas and is on the way to becoming a de facto standard because of its reasonably clear semantics and its standardized library.However, Java contains novel language features, which are not yet fully understood.More importantly, Java supports a novel paradigm for program deployment, and improves interactivity, portability and manageability.This paradigm opens new possibilities for abuse and causes concern about security.The ECOOP 2000 workshop on Formal Techniques for Java Programs was held in Sophia Antipolis, France.It was a follow-up for last year's ECOOP workshop on the same topic [1] and the Formal Underpinnings of the Java Paradigm workshop held at OOPSLA '98 [2].Proceedings containing all the papers are available as a technical report of the Computer Science Department of the FernUniversität Hagen [3].This special issue contains extended and refereed versions of four papers, selected from the best papers presented at the workshop.Eva Rose and Kristoffer Rose suggest in their paper 'Java access protection through typing' the integration of a dedicated read-only field access into the Java type system.The advantage is that

We propose a calculus describing compilation and linking in terms of operations on fragments, i.e. compilation units, without reference to their specific contents. We believe this calculus faithfully reflects the situation within modern programming systems. Binary compatibility in Java prescribes conditions under which modification of fragments does not necessitate recompilation of importing fragments. We apply our calculus to formalize binary compatibility, and demonstrate that several interpretations of the language specification are possible, each with different ramifications. We choose a particular interpretation, justify our choice, formulate and prove properties important for language designers and code library developers.

Separate compilation allows the decomposition of programs into units that may be compiled separately, and linked into an executable. Traditionally, separate compilation was equivalent to the compilation of all units together, and modification and re-compilation of one unit required re-compilation of all importing units.Java suggests a more flexible framework, in which the linker checks the integrity of the binaries to be combined. Certain source code modifications, such as addition of methods to classes, are defined as binary compatible. The language description guarantees that binaries of types (i.e. classes or interfaces) modified in binary compatible ways may be re-compiled and linked with the binaries of types that imported and were compiled using the earlier versions of the modified types.However, this is not always the case: some of the changes considered by Java as binary compatible do not guarantee successful linking and execution. In this paper we study the concepts around binary compatibility. We suggest a formalization of the requirement of safe linking and execution without re-compilation, investigate alternatives, demonstrate several of its properties, and propose a more restricted definition of binary compatible changes. Finally, we prove for a substantial subset of Java, that this restricted definition guarantees error-free linking and execution.

No abstract available.

This paper describes the integrated engineering study scheme, based around a set of 4 year MEng programmes of study, established by Imperial College. The paper outlines the rationale for the scheme and gives an account of its constituent programmes of study and the curriculum. The organisation and pattern of teaching, student workload and assessment methods are discussed. A detailed comparison of the scheme with the proposals and recommendations of the important model curricula are given.