Dala is a novel capability-based programming model that ensures data-race freedom while also supporting efficient inter-thread communication. While Dala has been designed to inform the design of future programming languages, the question arises whether existing languages can be retrofitted with Dala capabilities. We report such a design called JDala. In JDala, Dala capabilities are added to Java using annotations and interpreted using bytecode instrumentation. With some examples we demonstrate that by adding three simple annotations to the language, we can avoid concurrency bugs like deadlocks and unexpected program behaviour resulting from shallow immutability of Java standard library APIs. JDala demo: https://youtu.be/QddK1q35h-U

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.

Dala is a design for a concurrent dynamic object-oriented language. A key goal of Dala's design is to avoid data races, by ensuring threads do not share mutable state. In this paper we discuss our experience using the program verification tool Dafny to validate Dala's design. We explain how we modelled salient features of Dala in Dafny, and how Dafny did (or did not) assist our confidence in Dala's design.

Virtual Machines, Dynamic Compllers, and Implementation Frameworks make dynamic langauges easier and more efficient to optimize. Meanwhile, IDEs, provers, dependent types, type inferencers, and (so-called) “generative AI” mean programmers can express - statically - more information about the dynamic behaviour of their programs. Component libraries in these languages will come with assertions and proofs of their behaviour, and their advocates fantasise about transforming programming into the composition of dependently-typed higher-order yoneda morphisms, ensuring programs are correct-by-construction (where that construction is carried out by yet more generative AI). In this talk, I’ll speculate about what the resulting world will be like for programmers. Rather than a static world of platonic mathematical abstractions, I argue that the opposite will be true: that all languages will be dynamic.

Programming languages are languages --- “unnatural” languages because they are constructed explicitly; “formal” languages because they rely on mathematical notations and are described mathematically; “machine” languages because they are used to communicate with machines. Above all, programming languages are “human” languages. Programs in programming languages are spoken and read and written and designed and debugged and debated by humans, supported by human communities and forming those communities in turn. Langauge implementations, being programs themselves, are likewise designed and debugged and debated by humans.

Verona is a concurrent object-oriented programming language that organises all the objects in a program into a forest of isolated regions. Memory is managed locally for each region, so programmers can control a program's memory use by adjusting objects' partition into regions, and by setting each region's memory management strategy. A thread can only mutate (allocate, deallocate) objects within one active region---its "window of mutability". Memory management costs are localised to the active region, ensuring overheads can be predicted and controlled. Moving the mutability window between regions is explicit, so code can be executed wherever it is required, yet programs remain in control of memory use. An ownership type system based on reference capabilities enforces region isolation, controlling aliasing within and between regions, yet supporting objects moving between regions and threads. Data accesses never need expensive atomic operations, and are always thread-safe.

Rust successfully applies ownership types to control memory allocation. Unfortunately, Rust’s ownership restricts the programs’ topologies to the point where doubly-linked lists cannot be programmed in Safe Rust. We sketch how more flexible “local” ownership could be added to Rust, permitting multiple mutable references to objects, provided each reference is bounded by the object’s lifetime. To maintain thread-safety, locally owned objects must remain thread-local; to maintain memory safety, local objects must remain allocated until their owner’s lifetime expires.

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.

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.

Summary Though some software development teams are highly effective at delivering security, others either do not care or do not have access to security experts to teach them how. Unfortunately, these latter teams are still responsible for the security of the systems they build: systems that are ever more important to ever more people. We propose that a series of lightweight interventions, six hours of facilitated workshops delivered over three months, can improve a team's motivation to consider security and awareness of assurance techniques, changing its security culture even when no security experts are involved. The interventions were developed after an Appreciative Inquiry and Grounded Theory survey of security professionals to find out what approaches work best. We tested the interventions in a participatory action research field study where we delivered the workshops to three software development organizations and evaluated their effectiveness through interviews beforehand, immediately afterwards, and after twelve months. We found that the interventions can be effective with teams with limited or no security experience and that improvement is long‐lasting. This approach and the learning points arising from the work here have the potential to be applied in many development teams, improving the security of software worldwide.

Since LISP, dynamic languages have supported dynamically-checked type annotations. Even in dynamic languages, these annotations are typically static: tests are restricted to checking low-level features of objects and values, such as primitive types or membership of an explicit programmer-defined class.

Abstract As teams and organisations make the difficult shift to agile ways of working, there has been relatively little investigation of how they adopt and use agile practices. To aid those teams looking to move to agile we should examine how others have done so and what practical value they found. We studied teams which adopted agile practices across a spectrum from taking on a whole methodology to a couple of practices at a time, and then committed to continuous assessment and improvement of their ways of working. Those teams favoured adapting agile-based, team-oriented practices suited to their particular needs over technical practices and defined methodologies.

We know very little about why developers do what they do. Lab studies are all very well, but often their results (e.g. that static type systems make development faster) seem contradicted by practice (e.g. developers choosing JavaScript or Python rather than Java or C#). In this paper we build a first cut of a theory of why developers do what they do with a focus on the domain of static versus dynamic programming languages. We used a qualitative research method - Grounded Theory, to interview a number of developers \pmb(n=15) about their experience using static and dynamic languages, and constructed a Grounded Theory of their programming language choices.

Agile adoption is typically understood as a one-off organizational process involving a staged selection of agile development practices. This view of agility fails to explain the differences in the pace and effectiveness of individual teams transitioning to agile development. Based on a Grounded Theory study of 31 agile practitioners drawn from 18 teams across five countries, we present a grounded theory of becoming agile as a network of on-going transitions across five dimensions: software development practices, team practices, management approach, reflective practices, and culture. The unique position of a software team through this network, and their pace of progress along the five dimensions, explains why individual agile teams present distinct manifestations of agility and unique transition experiences. The theory expands the current understanding of agility as a holistic and complex network of on-going multidimensional transitions, and will help software teams, their managers, and organizations better navigate their individual agile journeys.

Which comes first: the object or the class? Language designers enjoy the conceptual simplicity of object-based languages (such as Emerald or Self) while many programmers prefer the pragmatic utility of classical inheritance (as in Simula and Java). Programmers in object-based languages have a tendency to build libraries to support traditional inheritance, and language implementations are often contorted to the same end. In this paper, we revisit the relationship between classes and objects. We model various kinds of inheritance in the context of an object-oriented language whose objects are not defined by classes, and explain why class inheritance and initialisation cannot be easily modelled purely by delegation.

Programmers’ lack of knowledge and interest in secure development threatens everyone who uses mobile apps. The rise of apps has engaged millions of independent app developers, who rarely encounter any but low level security techniques. But what if software security were presented as a game, or a story, or a discussion? What if learning app security techniques could be fun as well as empowering? Only by introducing the powerful motivating techniques developed for other disciplines can we hope to upskill independent app developers, and achieve the security that we’ll need in 2025 to safeguard our identities and our data.

Method names with multiple separate parts are a feature of many dynamic languages derived from Smalltalk. Generalising the syntax of method names to allow parts to be repeated, optional, or alternatives, means a single definition can respond to a whole family of method requests. We show how generalising method names can support flexible APIs for domain-specific languages, complex initialisation tasks, and control structures defined in libraries. We describe how we have extended Grace to support generalised method names, and prove that such an extension can be integrated into a gradually-typed language while preserving type soundness.

Combinations of structural and nominal object typing in systems such as Scala, Whiteoak, and Unity have focused on extending existing nominal, class-based systems with structural subtyping. The typical rules of nominal typing do not lend themselves to such an extension, resulting in major modifications. Adding object branding to an existing structural system integrates nominal and structural typing without excessively complicating the type system. We have implemented brand objects to explicitly type objects, using existing features of the structurally typed language Grace, along with a static type checker which treats the brands as nominal types. We demonstrate that the brands are useful in an existing implementation of Grace, and provide a formal model of the extension to the language.

The tension between software architecture and agility is not well understood by agile practitioners or researchers. If an agile software team spends too little time designing architecture up-front then the team faces increased risk and higher chance of failure, if the team spends too much time the delivery of value to the customer is delayed, and responding to change can become extremely difficult. This paper presents a grounded theory of agile architecture that describes how agile software teams answer the question of how much upfront architecture design effort is enough. This theory, based on grounded theory research involving 44 participants, presents six forces that affect the team's context and five strategies that teams use to help them determine how much effort they should put into up-front design.

Grace is a new gradually, structurally typed object-oriented programming language. Formal models of existing languages provide a rigorous base for claiming type soundness, so we have set about creating a model of a subset of Grace. While much of the formal literature of objects has used structural typing, models of popular modern languages such as Featherweight Java have had to use nominal typing to match the language they are modelling. In contrast to this, we present Tinygrace: a subset of Grace with a structural type system, feature-parity with FJ, and an accompanying proof of soundness.

The Escrow Exchange Contract has been used as a case study of building up complex and trustworthy systems from basic object capabilities, in the context of concurrent and distributed programming. In this short paper we present a Rational Reconstruction of the Escrow Exchange Contract case study, expressed in Grace, concentrating on the most essential issues of trustworthiness, and ignoring issues to do with distribution or more complex protocols. We then use our notation for capability policies to specify the key features of the reconstructed case study.

Jigsaw puzzle programming environments manipulate programs primarily by drag-and-drop. Generally these environments are based on their own special-purpose languages, meaning students must move on to another language as their programs grow. Tiled Grace is a tile-based editor for Grace, an educational programming language with a conventional textual syntax. Using Tiled Grace, programmers can move seamlessly between visualising their programs as tiles or source code, editing their programs via tiles or text, and continue on to traditional textual environments, all within the same programming language. We conducted a user experiment with Tiled Grace, and present the results of that experiment showing that users find dual views helpful.

LittleBits (little Bits.cc) is an open-source hardware library of pre-assembled analogue components that can be easily assembled into circuits, disassembled, reassembled, and re-used. In this paper, we consider littleBits - and the littleBits SynthKit in particular -- as a physically-embodied domain specific programming language. We describe the littleBits system, explain how littleBits "programs" are constructed as configurations of physical modules in the real world, and describe how they are typically used to control physical artefacts or constructions. We then argue that littleBits constructions essentially "visualise themselves". We describe how littleBits' liveness, embodiment, and plasticity assists both learning and debugging, and then evaluate littleBits configurations according to the cognitive dimensions of notations.

Many programming language constructs that support software engineering in the large - explicit variable declarations, explicit external dependencies, static types, information hiding, invariants-provide little benefit to the small programs written by novice programmers, where every extra syntactic token has to be explained and understood before novices can succeed in running even the simplest program. We are designing Grace, a new educational object-oriented language that we hope will prove useful for teaching both programming and software engineering. This paper describes some of the tradeoffs between teaching programming and teaching software engineering that we faced while designing Grace, and our attempts to address those tradeoffs.

The object-capability model is one of the industry standards adopted for the implementation of security policies for web-based software. Object-capabilities in various forms are supported by programming languages such as E, Joe-E, Newspeak, Grace, and the newer versions of Javascript. Unfortunately, code written using capabilities tends to concentrate on the low-level mechanism rather than the high-level policy.

Agile teams advocates face-to-face conversation, frequent communication and close collaboration between team members in order to work together as one team. In distributed software development, however, separation through space, time and culture affects the ability of the members of a distributed team to work together as one team. Through a Grounded Theory study that involved 55 participants from 38 different software companies in the USA, India and Australia, we investigate key concerns of distributed teams in Agile software development. We found that distributed teams need significant support from senior management in terms of organisational culture, human resource management, financial sponsorship, infrastructure and technology, and customer liaison. In this paper, we discuss the importance of senior management support for Agile software development with distributed teams.

Object ownership enforces encapsulation within object-oriented programs by forbidding incoming aliases into objects' representations. Many common data structures, such as collections with iterators, require incoming aliases, so there has been much work on relaxing ownership's encapsulation to permit multiple incoming aliases. This research asks the opposite question: Are your aliases really necessary? In this paper, we count the cost of programming with strong object encapsulation. We refactored the JDK 5.0 collection classes so that they did not use incoming aliases, following either the owner-as-dominator or the owner-as-accessor encapsulation discipline. We measured the performance time overhead the refactored collections impose on a set of microbenchmarks and on the DaCapo, SPECjbb and SPECjvm benchmark suites. While the microbenchmarks show that individual operations and iterations can be significantly slower on encapsulated collection (especially for owner-as-dominator), we found less than 3% slowdown for owner-as-accessor across the large scale benchmarks. As a result, we propose that well-known design patterns such as Iterator commonly used by software engineers around the world need to be adjusted to take ownership into account. As most design patterns are used as a building block in constructing larger pieces of software, a small adjustment to respect ownership will not have any impact on the productivity of programmers but will have a huge impact on the quality of the resulting code with respect to aliasing.

Grace is a new object-oriented language that supports a variety of approaches to teaching programming. It integrates accepted new ideas in programming languages into a simple language that allows students and teachers to focus on the essential complexities of programming rather than the accidental complexities of the language. We motivate Grace, review its design, and evaluate it against Kolling's criteria.

Most software development tools and applications are designed from a single-user perspective and are bound to the desktop and Integrated Development Environments (IDEs). These tools and applications make it hard for developers to analyse and interact with software artifacts collaboratively. We present SourceVisa multi-user collaborative software visualization application for use on large multi-touch tables. We describe the design and visualization features of SourceVis, present findings from a user study, and discuss the implications for building collaborative software visualization applications.

“Jigsaw puzzle” programming environments manipulate programs primarily by drag-and-drop. Generally these environments are based on their own special-purpose languages, meaning students must move on to another language as their programs grow. Tiled Grace is a tile-based editor for Grace, an educational programming language with a conventional textual syntax. Using Tiled Grace, programmers can move seamlessly between visualising their programs as tiles or source code, editing their programs via tiles or text, and continuing on to traditional textual environments, all within the same programming language.

Self-organizing teams have been recognized and studied in various forms-as autonomous groups in socio-technical systems, enablers of organizational theories, agents of knowledge management, and as examples of complex-adaptive systems. Over the last decade, self-organizing teams have taken center stage in software engineering when they were incorporated as a hallmark of Agile methods. Despite the long and rich history of self-organizing teams and their recent popularity with Agile methods, there has been little research on the topic within software wngineering. Particularly, there is a dearth of research on how Agile teams organize themselves in practice. Through a Grounded Theory research involving 58 Agile practitioners from 23 software organizations in New Zealand and India over a period of four years, we identified informal, implicit, transient, and spontaneous roles that make Agile teams self-organizing. These roles-Mentor, Coordinator, Translator, Champion, Promoter, and Terminator-are focused toward providing initial guidance and encouraging continued adherence to Agile methods, effectively managing customer expectations and coordinating customer collaboration, securing and sustaining senior management support, and identifying and removing team members threatening the self-organizing ability of the team. Understanding these roles will help software development teams and their managers better comprehend and execute their roles and responsibilities as a self-organizing team.

Object orientation and pattern matching are often seen as conflicting approaches to program design. Object-oriented programs place type-dependent behavior inside objects and invoke it via dynamic dispatch, while pattern-matching programs place type-dependent behavior outside data structures and invoke it via multiway conditionals (case statements).

Background: Trust fuels team performance and contributes to build an effective and cohesive team. The self-organizing and collaborative nature of Agile teams increases the importance of trust in software development teams. Trust is, however, affected in distributed teams. Aim: Through a Grounded Theory study we investigate the impact of trust in distributed Agile teams. Method: We interviewed 45 Agile practitioners from 28 different software companies in the USA, India and Australia, over a period of 3 years, using semi-structured open-ended questions. Results: In this paper, we present the reasons for lack of trust and its adverse effects in distributed Agile teams that emerged from the analysis, using the causal-consequences theoretical model. Conclusion: Understanding the causes and consequences of lack of trust can develop awareness of the importance of trust in distributed teams and pave ways for effectively building trust in project-oriented contexts.

Grounded Theory (GT) is gaining popularity as research method in Software Engineering; however, it is still not widely understood. We present some patterns based on the use of GT to study Software Engineering contexts including our own experiences of applying classic GT in an attempt to make it more accessible for Software Engineering researchers (aka 'geeks').

In order to increase our ability to use measurement to support software development practise we need to do more analysis of code. However, empirical studies of code are expensive and their results are difficult to compare. We describe the Qualitas Corpus, a large curated collection of open source Java systems. The corpus reduces the cost of performing large empirical studies of code and supports comparison of measurements of the same artifacts. We discuss its design, organisation, and issues associated with its development.

Agile teams are described as "self-organizing". How these teams actually organize themselves in practice, however, is not well understood. Through Grounded Theory research involving 24 Agile practitioners across 14 software organizations in New Zealand and India, we identified six informal roles that team members adopt in order to help their teams self-organize. These roles --- Mentor, Co-ordinator, Translator, Champion, Promoter, and Terminator --- help teams learn Agile practices, liaise with customers, maintain management support, and remove ineffective team members. Understanding these roles will help software teams become self-organizing, and should guide Agile coaches in working with Agile teams.

Tribal Ownership unifies class nesting and object ownership. Tribal Ownership is based on Tribe, a language with nested classes and object families. In Tribal Ownership, a program's runtime object ownership structure is characterised by the lexical nesting structure of its classes.We build on a variant of Tribe to present a descriptive ownership system, using object nesting to describe heap partitions, but without imposing any restrictions on programming disciplines. We then demonstrate how a range of different prescriptive ownership policies can be supported on top of the descriptive Tribal Ownership mechanism; including a novel owners-as-local-dominators policy. We formalise our type system and prove soundness and several ownership invariants. The resulting system requires strikingly few annotations, and uses well-understood encapsulation techniques to create ownership systems that should be intuitive for programmers.

Evangelists for Agile methods strongly encourage all projects to follow every practice of their chosen method. Based on a Grounded Theory study involving 40 participants at 16 organizations, and corroborated by 4 independent case studies, we argue that development methods and practices must be adapted to fit their contexts. Understanding Agility in context will help development teams, their managers, and Agile coaches to adapt development processes to fit their projects' contexts.

Pluggable types enable users to enforce multiple type systems in one programming language. We have developed a suite of tools, called the JavaCOP framework, that allows developers to create pluggable type systems for Java. JavaCOP provides a simple declarative language in which program constraints are defined over a program's abstract syntax tree. The JavaCOP compiler automatically enforces these constraints on programs during compilation. The JavaCOP framework also includes a dataflow analysis API in order to support type systems which depend on flow-sensitive information. Finally, JavaCOP includes a novel test framework which helps users gain confidence in the correctness of their pluggable type systems. We demonstrate the framework by discussing a number of pluggable type systems which have been implemented in JavaCOP in order to detect errors and enforce strong invariants in programs. These type systems range from general-purpose checkers, such as a type system for nonnull references, to domain-specific ones, such as a checker for conformance to a library's usage rules.

Large, unwieldy classes are a significant maintenance problem. Programmers dislike them because the fundamental logic is often obscured, making them hard to understand and modify. This paper proposes a solution - a semi-automatic technique for splitting large classes into smaller, more cohesive ones. The core of the technique is the use of betweenness clustering to identify the best way of partitioning a class. This turned a tedious manual process into a quick and simple semi-automated one in roughly one third of the cases we examined.

Multiple dispatch uses the run time types of more than one argument to a method call to determine which method body to run. While several languages over the last 20 years have provided multiple dispatch, most object-oriented languages still support only single dispatch forcing programmers to implement multiple dispatch manually when required. This paper presents an empirical study of the use of multiple dispatch in practice, considering six languages that support multiple dispatch, and also investigating the potential for multiple dispatch in Java programs. We hope that this study will help programmers understand the uses and abuses of multiple dispatch; virtual machine implementors optimise multiple dispatch; and language designers to evaluate the choice of providing multiple dispatch in new programming languages.

Many contemporary object-oriented programming languages support first-class queries or comprehensions. These language extensions make it easier for programmers to write queries, but are generally implemented no more efficiently than the code using collections, iterators, and loops that they replace. Crucially, whenever a query is re-executed, it is recomputed from scratch. We describe a general approach to optimising queries over mutable objects: query results are cached, and those caches are incrementally maintained whenever the collections and objects underlying those queries are updated. We hope that the performance benefits of our optimisations may encourage more general adoption of first-class queries by object-oriented programmers.

Software visualization has always been expensive, special purpose, and hard to program. Most of the existing software visualization tools require too much time for end-user developers to learn and make effective use of. We are currently building a Web software visualization application that allows end-user to create, view, save, and share visualizations. In this abstract we introduce our software corpus visualization project and summarize our results thus far.

Object aliasing causes as many problems in dynamic languages as it does in static languages. Most existing work on aliasing, such as ownership types, relies on static checking based on annotations and type declarations. We introduce ConstraintedJava, a scripting language based on BeanShell that provides dynamic ownership checking. Dynamic ownership provides the encapsulation benefits of static ownership types but preserves the flexibility of dynamic languages.

Existing ownership type systems require objects to have precisely one primary owner, organizing the heap into an ownership tree. Unfortunately, a tree structure is too restrictive for many programs, and prevents many common design patterns where multiple objects interact.

Current human–computer interaction (HCI) research into video games rarely considers how they are different from other forms of software. This leads to research that, while useful concerning standard issues of interface design, does not address the nature of video games as games specifically. Unlike most software, video games are not made to support external, user-defined tasks, but instead define their own activities for players to engage in. We argue that video games contain systems of values which players perceive and adopt, and which shape the play of the game. A focus on video game values promotes a holistic view of video games as software, media, and as games specifically, which leads to a genuine video game HCI.

Pluggable types have been proposed to support multiple type systems in the same programming language. We have designed and implemented JavaCOP, a program constraint system for implementing practical pluggable type systems for Java. JavaCOP enforces user-defined typing constraints written in a declarative and expressive rule language. We have validated our design by (re)implementing a range of type systems and program checkers. By using a program constraint system to implement pluggable types, programmers are able to check that their programs will operate correctly in restricted environments, adhere to strict programming rules, avoid null pointer errors or scoped memory exceptions, and meet style guidelines, while programming language researchers can easily experiment with novel type systems.

Large amounts of Java software have been written since the language's escape into unsuspecting software ecology more than ten years ago. Surprisingly little is known about the structure of Java programs in the wild: about the way methods are grouped into classes and then into packages, the way packages relate to each other, or the way inheritance and composition are used to put these programs together. We present the results of the first in-depth study of the structure of Java programs. We have collected a number of Java programs and measured their key structural attributes. We have found evidence that some relationships follow power-laws, while others do not. We have also observed variations that seem related to some characteristic of the application itself. This study provides important information for researchers who can investigate how and why the structural relationships we find may have originated, what they portend, and how they can be managed.

Ownership types enforce encapsulation in object-oriented programs by ensuring that objects cannot be leaked beyond object(s) that own them. Existing ownership programming languages either do not support parametric polymorphism (type genericity) or attempt to add it on top of ownership restrictions. Generic Ownership provides per-object ownership on top of a sound generic imperative language. The resulting system not only provides ownership guarantees comparable to established systems, but also requires few additional language mechanisms due to full reuse of parametric polymorphism. We formalise the core of Generic Ownership, highlighting that only restriction of this calls and owner subtype preservation are required to achieve deep ownership. Finally we describe how Ownership Generic Java (OGJ) was implemented as a minimal extension to Generic Java in the hope of bringing ownership types into mainstream programming.

Existing approaches to object encapsulation either rely on ad hoc syntactic restrictions or require the use of specialised type systems. Syntactic restrictions are difficult to scale and to prove correct, while specialised type systems require extensive changes to programming languages. We demonstrate that confinement can be enforced cheaply in Featherweight Generic Java, with no essential change to the underlying language or type system. This result demonstrates that polymorphic type parameters can simultaneously act as ownership parameters and should facilitate the adoption of confinement and ownership type systems in general-purpose programming languages.

When researchers extend a conventional communication application to mobile devices, the communication becomes ubiquitous. We recently examined a mobile communication application from a usability perspective. We found that despite the potentially high utility of the mobile communication application, it had usability issues that required user interface redesign. This paper is an alert for mobile and ubiquitous multimedia designers that they must not ignore usability considerations when designing software and hardware solutions for ubiquitous mobility.

A memory model based on scoped areas is one of the distinctive features of the Real-Time Specification for Java (RTSJ). Scoped types ensure timely reclamation of memory and predictable performance. The price to pay for these benefits is an unfamiliar programming model that, at the same time, is complex, requires checking all memory accesses, and rewards design-time errors with run-time crashes. We investigate an alternative approach, referred to as scoped types, that simplifies the task of managing memory in real-time codes. The key feature of our proposal is that the run-time partition of memory imposed by scoped areas is straightforwardly mirrored in the program text. Thus cursory inspection of a program reveals which objects inhabit the different scopes, significantly simplifying the task of understanding real-time Java programs. Moreover, we introduce a type system which ensures that no run-time errors due to memory access checks occur. Thus a RTSJ-compliant virtual machine does not require memory access checks. The contributions of this paper are the concept of scoped types, and a proof soundness of the type system. Experimental results are described in future work.

Abstract A number of proposals to manage aliasing in Java‐like programming languages have been advanced over the last five years. It is not clear how practical these proposals are, that is, how well they relate to the kinds of programs currently written in Java‐like languages. To address this problem, we analysed heap snapshots from a corpus of Java programs. Our results indicate that object‐oriented programs do in fact exhibit symptoms of encapsulation in practice, and that proposed models of uniqueness, ownership, and confinement can usefully describe the aliasing structures of object‐oriented programs. Understanding the kinds of aliasing present in programs should help us to design formalisms to make explicit the kinds of aliasing implicit in object‐oriented programs. Copyright © 2004 John Wiley & Sons, Ltd.

The Enterprise JavaBeans (EJB) framework requires developers to preserve architectural integrity constraints when writing EJB components. Breaking these constraints allows components to violate the transaction protocol, bypass security mechanisms, disable object persistence, and be susceptible to malicious attacks from other EJBs. We present an object confinement discipline that allows static verification of components' integrity as they are deployed into an EJB server. The confinement rules are simple for developers to understand, require no annotation to the code of EJB components, and can be efficiently enforced in existing EJB servers.

Aliasing in object-oriented systemsAliasing is naturally endemic in object-oriented programs.Every object in an object-oriented program can refer to many other objects, so the overall topology of a program is a general graph.The state of an object can rely on the states of all of the other objects it references.Aliasing occurs when one object is reachable via multiple paths, usually because it is referenced by several other objects.Aliasing results in 'action at a distance'-operations on one object can affect the logical state of apparently unrelated objects that (perhaps indirectly) refer to it.The articles in this issue address the costs and benefits of aliasing in a number of ways.The first three articles focus on programming techniques and language features that allow programmers to control aliasing and its effects.Boris Bokowski and Jan Vitek describe how Confined Types can be used to restrict potential aliasing within programs.John Boyland's article on Alias Burying describes how variables holding unique references to objects can be implemented without special programming language support.Günther Kniesel and Dirk Theisen describe how Java can be extended to support types that provide read-only access to objects, thus eliminating some of the unwanted effects of aliasing without restricting the program's topology.While new languages and language features can help reduce and control aliasing, compilers today must deal with programs filled with potential aliases.The article by Anthony Hosking et al. describes how partial redundancy elimination can support compiler-level optimizations in the presence of aliasing.Finally, Olivier Zenda and Dominque Colnet evaluate the use of aliasing in the implementation of the SmallEiffel compiler.This issue, then, represents the state of practice in dealing with aliasing in object-oriented systems.

Designing concurrent object-oriented programs is hard. Correct programs must coordinate multiple threads accessing composite objects, using low-level mechanisms such as locks and read-write sets. Efficient programs must balance the complexity and overhead of the coordination mechanisms against the increased performance possible through concurrency. A method-level algebra of exclusion provides a succinct description of the conditions under which a thread must be excluded from a component of a composite object. Using the algebra, programmers can check whether their programs meet their exclusion requirements, can eliminate redundant exclusion controls, and can remove synchronisation overhead by reducing concurrency.

If an object-oriented program is a collection of communicating objects, then the objects' protocols define the languages the program speaks. Unfortunately, protocols are difficult to design in isolation, so many programs' protocols are not as well designed as they could be. This paper presents six patterns which describe how objects' protocols can be designed or redesigned, by considering the arguments the protocols accept and the results the protocols return. By using these patterns, programs and designs can be made simpler, more general, and easier to change.

Object-oriented programming languages allow inter-object aliasing. Although necessary to construct linked data structures and networks of interacting objects, aliasing is problematic in that an aggregate object's state can change via an alias to one of its components, without the aggregate being aware of any aliasing.Ownership types form a static type system that indicates object ownership. This provides a flexible mechanism to limit the visibility of object references and restrict access paths to objects, thus controlling a system's dynamic topology. The type system is shown to be sound, and the specific aliasing properties that a system's object graph satisfies are formulated and proven invariant for well-typed programs.