Class invariants—consistency constraints preserved by every operation on objects of a given type—are fundamental to building, understanding, and verifying object-oriented programs. For verification, however, they raise difficulties, which have not yet received a generally accepted solution. The present work introduces a proof rule meant to address these issues and allow verification tools to benefit from invariants. It clarifies the notion of invariant and identifies the three associated problems: callbacks, furtive access, and reference leak. As an example, the 2016 Ethereum DAO bug, in which $50 million was stolen, resulted from a callback invalidating an invariant. The discussion starts with a simplified model of computation and an associated proof rule, demonstrating its soundness. It then removes one by one the three simplifying assumptions, each removal raising one of the three issues and leading to a corresponding adaptation to the proof rule. The final version of the rule can tackle tricky examples, including “challenge problems” listed in the literature.

Abstract A successful automated program proof is, in software verification, the ultimate triumph. In practice, however, the road to such success is paved with many failed proof attempts. Unlike a failed test, which provides concrete evidence of an actual bug in the program, a failed proof leaves the programmer in the dark. Can we instead learn something useful from it? The work reported here takes advantage of the rich information that some automatic provers internally collect about the program when attempting a proof. If the proof fails, the Proof2Test tool presented in this article uses the counterexample generated by the prover (specifically, the SMT solver underlying the Boogie tool used in the AutoProof system to perform correctness proofs of contract‐equipped Eiffel programs) to produce a failed test, which provides the programmer with immediately exploitable information to correct the program. The discussion presents Proof2Test and the application of the ideas and tool to a collection of representative examples.

Existing techniques of Design by Contract do not allow software developers to specify complete contracts in many cases. Incomplete contracts leave room for malicious implementations. This article complements Design by Contract with a simple yet powerful technique that removes the problem without adding syntactical mechanisms. The proposed technique makes it possible not only to derive complete contracts, but also to rigorously check and improve completeness of existing contracts without instrumenting them.

Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adoption, however, is the difficulty of programming them and the low-level control of the hardware required to achieve good performance. This paper suggests a programming library, SafeGPU, that aims at striking a balance between programmer productivity and performance, by making GPU data-parallel operations accessible from within a classical object-oriented programming language. The solution is integrated with the design-by-contract approach, which increases confidence in functional program correctness by embedding executable program specifications into the program text. We show that our library leads to modular and maintainable code that is accessible to GPGPU non-experts, while providing performance that is comparable with hand-written CUDA code. Furthermore, runtime contract checking turns out to be feasible, as the contracts can be executed on the GPU.

We present the integration of the AutoFix automated program repair technique into the EiffelStudio Development Environment. AutoFix presents itself like a recommendation system capable of automatically finding bugs and suggesting fixes in the form of source-code patches. Its performance suggests usage scenarios where it runs in the background or during work interruptions, displaying fix suggestions as they become available. This is a contribution towards the vision of semantic Integrated Development Environments, which offer powerful automated functionality within interfaces familiar to developers. A screencast highlighting the main features of AutoFix can be found at: http://youtu.be/Ff2ULiyL-80.

This paper presents a new, multidisciplinary robotics programming course, reports initial results, and describes subsequent improvements. With equal emphasis on software engineering and robotics, the course teaches students how software engineering applies to robotics. Students learn independently and interactively and gain hands-on experience by implementing robotics algorithms on a real robot. To understand the effects of the course, we conducted an exit and an 8-month survey and measured software quality of the students' solutions. The analysis shows that the hands-on experience helped everyone learn and retain robotics well, but the students' knowledge gain in software engineering depended on their prior programming knowledge. Based on these findings, we propose improvements to the course. Lastly, we reflect our experience on andragogy, minimalism, and interactive learning.

This paper presents SmartWalker and evaluates the appropriateness and usefulness of the walker and its gesture-based interface for the elderly. As a high-tech extension of a regular walker, the SmartWalker aims to assist its user intelligently and navigate around its environment autonomously. Equipped with sensors and actuators, the prototype accepts gesture commands and navigates around accordingly. The gesture-based interface uses a k-nearest neighbours classifier with dynamic time warping to recognize gestures and the Viola and Jones face detector to locate the user. We evaluated the walker with 23 residents and eight staff members at five different retirement homes in Zurich. The elderly found the SmartWalker useful and exciting, but few were willing to replace their walkers by robotic walkers. Their reluctance may stem from the walker's size and weight and their unfamiliarity with technology.

Software design patterns are reusable solutions to commonly occurring problems in software development. Growing complexity of robotics software increases the importance of applying proper software engineering principles and methods such as design patterns to robotics. Concurrency design patterns are particularly interesting to robotics because robots often have many components that can operate in parallel. However, there has not yet been any established set of reusable concurrency design patterns for robotics. For this purpose, we choose six known concurrency patterns - Future, Periodic timer, Invoke later, Active object, Cooperative cancellation, and Guarded suspension. We demonstrate how these patterns could be used for solving common robotic coordination tasks. We also discuss advantages and disadvantages of the patterns and how existing robotics programming frameworks can support them.

The advent of Massive Open Online Courses makes it essential to develop tools and techniques that automatically support computer science students in solving programming assignments. Complementing existing tools for automatically checking the correctness of students' programs, we have developed and evaluated an incremental hint system for programming exercises. The hint system displays, upon request from a student, a series of hints on how to approach a solution. The hints are created in advance from the source code of the exercise's reference solution using our hint generation tool. This tool can run in fully automatic mode, where hints reveal more and more parts of the solution code; in manual mode, where teachers can customize hints by annotating the input source code; and in a combination of the two modes. We evaluated the hint system throughout our Introduction to Programming course which provides a companion online course. The findings suggest that students who needed assistance with an exercise used the hint system and found it helpful to guide them through the process of building a solution.

Making threaded programs safe and easy to reason about is one of the chief difficulties in modern programming. This work provides an efficient execution model and implementation for SCOOP, a concurrency approach that provides not only data-race freedom but also pre/postcondition reasoning guarantees between threads. The extensions we propose influence the underlying semantics to increase the amount of concurrent execution that is possible, exclude certain classes of deadlocks, and enable greater performance.

Making threaded programs safe and easy to reason about is one of the chief difficulties in modern programming. This work provides an efficient execution model for SCOOP, a concurrency approach that provides not only data-race freedom but also pre/postcondition reasoning guarantees between threads. The extensions we propose influence both the underlying semantics to increase the amount of concurrent execution that is possible, exclude certain classes of deadlocks, and enable greater performance. These extensions are used as the basis of an efficient runtime and optimization pass that improve performance 15x over a baseline implementation. This new implementation of SCOOP is, on average, also 2x faster than other well-known safe concurrent languages. The measurements are based on both coordination-intensive and data-manipulation-intensive benchmarks designed to offer a mixture of workloads.

The importance of planning and management skills in software development is very difficult to convey in software engineering courses. We present the synopsis of an assignment whose purpose is to demonstrate the significance of such skills, including effective communication, team coordination and collaboration, and overall project planning. The assignment is organized in the context of a distributed software engineering course carried out in collaboration with 12 universities in South America, Europe and Africa. The assignment is a globally distributed contest issued before most development activities related to the course's software project are performed, aiming at favoring the collaboration between students prior to project development. The contest does not involve any programming, and is not related to the project development activities. Instead, it consists of making teams in different countries compete in collaboratively solving a set of very simple tasks. The complexity of the activity is in team collaboration and coordination, and their lack is evident when the tasks are not correctly solved, or not solved in time. Despite the simplicity of the as-signment, students have found it useful in helping them understand the significance of management and planning challenges in distributed software development. Moreover, the assignment helped in team building, by creating a better team atmosphere and contributing in identifying team members better suited for management.

Collaborative software development requires programmers to coordinate their work and merge individual contributions into a consistent shared code base. Traditionally, coordination follows a series of update-modify-commit" cycles, where merge conflicts arise upon committing if individual modifications have diverged and must be explicitly reconciled. Researchers have been suggesting that providing timely awareness information about "who's changing what" may not only help deal with conflicts but, more generally, improve the effectiveness of collaboration. This paper investigates the impact of awareness information in the context of globally distributed software development. Based on an analysis of data from 105 student developers constituting 12 development teams located in different countries, we analyze, among other things: 1) the frequency of merge conflicts and insufficient awareness, 2) the impact of distribution on team awareness, 3) the perceived impact of conflicts and lack of awareness on productivity, motivation, and project punctuality. Our findings include: 1) lack of awareness occurs more frequently than merge conflicts, 2) information about remote team members is missing roughly as often as information about colocated ones, 3) insufficient awareness information affects more negatively programmer's performance than merge conflicts.

Concurrency is inherent to robots, and using concurrency in robotics can greatly enhance performance of the robotics applications. So far, however, the use of concurrency in robotics has been limited and cumbersome. This paper presents Roboscoop, a new robotics framework based on Simple Concurrent Object Oriented Programming (SCOOP). SCOOP excludes data races by construction, thereby eliminating a major class of concurrent programming errors. Roboscoop utilizes SCOOP's concurrency and synchronization mechanisms for coordination in robotics applications. We demonstrate Roboscoop's simplicity by comparing Roboscoop to existing middlewares and evaluate Roboscoop's usability by employing it in education.

MOOCs (Massive Open Online Courses), which have taken higher education by storm, are an opportunity to elevate the quality of existing residential courses. We report about an experimental attempt during the Autumn 2013 semester at ETH Zurich, involving our "Introduction to Programming" course. We designed and implemented a MOOC infrastructure and used it as a SPOC (Small Private Online Course) to support and complement the existing course. The results reported in this article are encouraging for two reasons: first, the participation level was good, in spite of the fact that the online course was an optional addition to the residential course; second, students really liked the assessments (quizzes and programming exercises), in spite of the fact that assessments did not count towards the course final grade. The data we collected suggest that this may, at least in part, be due to a gamification aspect we introduced in the course: awarding virtual badges for obtaining full points in the quizzes.

Summary form only given. In 2007, I had the honor of an invited presentation at MEMOCODE, where I discussed the frame problem: how to establish that programs do not modify certain properties. The problem is particularly challenging in the case of object-oriented programs involving complex pointer (reference) data structures. Seven years later, it is still largely an open problem, although significant progress has occurred. After realizing that a satisfactory solution requires addressing another difficult problem, alias analysis, I have devoted much of my work to program analysis techniques that tackle both aliasing and framing. Taking advantage of the kind invitation to present again at MEMOCODE, I will describe the current state of this work and how its results are embodied in program analysis tools that provide automatic means - not requiring program annotations - to ascertain fundamental properties of programs.

This paper describes AutoFix, an automatic debugging technique that can fix faults in general-purpose software. To provide high-quality fix suggestions and to enable automation of the whole debugging process, AutoFix relies on the presence of simple specification elements in the form of contracts (such as pre- and postconditions). Using contracts enhances the precision of dynamic analysis techniques for fault detection and localization, and for validating fixes. The only required user input to the AutoFix supporting tool is then a faulty program annotated with contracts; the tool produces a collection of validated fixes for the fault ranked according to an estimate of their suitability. In an extensive experimental evaluation, we applied AutoFix to over 200 faults in four code bases of different maturity and quality (of implementation and of contracts). AutoFix successfully fixed 42 percent of the faults, producing, in the majority of cases, corrections of quality comparable to those competent programmers would write; the used computational resources were modest, with an average time per fix below 20 minutes on commodity hardware. These figures compare favorably to the state of the art in automated program fixing, and demonstrate that the AutoFix approach is successfully applicable to reduce the debugging burden in real-world scenarios.

Developers face a wide choice of programming languages and libraries supporting multicore computing. Ever more diverse paradigms for expressing parallelism and synchronization become available while their influence on usability and performance remains largely unclear. This paper describes an experiment comparing four markedly different approaches to parallel programming: Chapel, Cilk, Go, and Threading Building Blocks (TBB). Each language is used to implement sequential and parallel versions of six benchmark programs. The implementations are then reviewed by notable experts in the language, thereby obtaining reference versions for each language and benchmark. The resulting pool of 96 implementations is used to compare the languages with respect to source code size, coding time, execution time, and speedup. The experiment uncovers strengths and weaknesses in all approaches, facilitating an informed selection of a language under a particular set of requirements. The expert review step furthermore highlights the importance of expert knowledge when using modern parallel programming approaches.

Modern software development extensively involves reusing library components accessed through their Application Programming Interfaces (APIs). Usability is therefore a fundamental goal of API design, but rigorous empirical studies of API usability are still relatively uncommon. In this paper, we present the design of an API usability study which combines interview questions based on the cognitive dimensions framework, with systematic observations of programmer behavior while solving programming tasks based on ``tokens''. We also discuss the implementation of the study to assess the usability of a persistence library API (offering functionalities such as storing objects into relational databases). The study involved 25 programmers (including students, researchers, and professionals), and provided additional evidence to some critical features evidenced by related studies, such as the difficulty of finding good names for API features and of discovering relations between API types. It also discovered new issues relevant to API design, such as the impact of flexibility, and confirmed the crucial importance of accurate documentation for usability.

Debugging - the process of finding and correcting programming mistakes - faces too the challenges of distributed and collaborative development. The debugging tools commonly used by programmers are integrated into traditional development environments such as Eclipse or Visual Studio, and hence do not offer specific features for collaboration or remote shared usage. In this paper, we describe CDB, a debugging technique and integrated tool specifically designed to support effective collaboration among developers during shared debugging sessions. We also discuss the design and results of an empirical study aimed at identifying features that can ameliorate the effectiveness of collaborative debugging processes, and at evaluating the usefulness of our CDB collaborative debugging approach. The study suggests that CDB's collaboration features are often perceived as important for effective debugging, and can improve the overall debugging experience in collaborative settings.

Experience with lightweight formal methods suggests that programmers are willing to write specification if it brings tangible benefits to their usual development activities. This paper considers stronger specifications and studies whether they can be deployed as an incremental practice that brings additional benefits without being unacceptably expensive. We introduce a methodology that extends Design by Contract to write strong specifications of functional properties in the form of preconditions, postconditions, and invariants. The methodology aims at being palatable to developers who are not fluent in formal techniques but are comfortable with writing simple specifications. We evaluate the cost and the benefits of using strong specifications by applying the methodology to testing data structure implementations written in Eiffel and C#. In our extensive experiments, testing against strong specifications detects twice as many bugs as standard contracts, with a reasonable overhead in terms of annotation burden and run-time performance while testing. In the wide spectrum of formal techniques for software quality, testing against strong specifications lies in a “sweet spot” with a favorable benefit to effort ratio.

Can the methods of empirical software engineering give us answers to the truly important open questions in the field?

With the wide support for object serialization in object-oriented programming languages, persistent objects have become commonplace and most large object-oriented software systems rely on extensive amounts of persistent data. Such systems also evolve over time. Retrieving previously persisted objects from classes whose schema has changed is, however, difficult, and may lead to invalidating the consistency of the application. The ESCHER framework addresses these issues through an IDE-integrated approach that handles class schema evolution by managing versions of the code and generating transformation functions automatically. The infrastructure also enforces class invariants to prevent the introduction of potentially corrupt objects. This paper describes a model for class attribute changes, a measure for class evolution robustness, four empirical studies, and the design and implementation of the ESCHER system.

Large parts of today's software systems are devoted to detecting and recovering from failures, making exception handling a critical issue in software development. Concurrent software complicates this issue: most concurrent programming languages require a mechanism to deal with asynchronous exceptions, but because of the diverse design choices underlying each language, no approach fits all situations. We introduce a classification of possible approaches to guide the development of asynchronous exception mechanisms, and we show its applicability by deriving a sound and comprehensible mechanism for SCOOP, an object-oriented programming model for concurrency. We describe the key idea of the mechanism using the accountability framework, which precisely defines the obligations of client and supplier regarding the reporting of exceptions. The framework not only provides the necessary intuition to apply the mechanism correctly, it is also useful to comprehend other approaches.

This paper presents a case study on the impact of development processes on the success of globally distributed software projects. The study compares agile (Scrum, XP, etc.) vs. structured (RUP, waterfall) processes to determine if the choice of process impacts: the overall success and economic savings of distributed projects; the importance customers attribute to projects; the motivation of the development teams; and the amount of real-time or asynchronous communication required during project development. The case study includes data from 66 projects developed in Europe, Asia, and the Americas. The results show no significant difference between the outcome of projects following agile processes and structured processes, suggesting that agile and structured processes can be equally effective for globally distributed development. The paper also discusses several qualitative aspects of distributed software development such as the advantages of near shore vs. offshore, the preferred communication patterns, and some common critical aspects.

Freefinement is an algorithm that constructs a sound refinement calculus from a verification system under certain conditions. In this paper, a verification system is any formal system for establishing whether an inductively defined term, typically a program, satisfies a specification. Examples of verification systems include Hoare logics and type systems. Freefinement first extends the term language to include specification terms, and builds a verification system for the extended language that is a sound and conservative extension of the original system. The extended system is then transformed into a sound refinement calculus. The resulting refinement calculus can interoperate closely with the verification system - it is even possible to reuse and translate proofs between them. Freefinement gives a semantics to refinement at an abstract level: it associates each term of the extended language with a set of terms from the original language, and refinement simply reduces this set. The paper applies freefinement to a simple type system for the lambda calculus and also to a Hoare logic.

Automated random testing is efficient at detecting faults but it is certainly not an optimal testing strategy for every given program. For example, an automated random testing tool ignores that some routines have stronger preconditions, they use certain literal values, or they are more error-prone. Taking into account such characteristics may increase testing effectiveness. In this article, we present Evotec, an enhancement of random testing which relies on genetic algorithms to evolve a best testing strategy for contract-equipped programs. The resulting strategy is optimized for detecting more faults, satisfying more routine preconditions and establishing more object states on a given set of classes to test. Our experiment tested 92 classes over 1710 hours. It shows that Evotec detected 29% more faults than random+ and 18% more faults than the precondition-satisfaction strategy.

Concurrency has been rapidly gaining importance in computing, and correspondingly in computing curricula. Concurrent programming is, however, notoriously hard even for expert programmers. New language designs promise to make it easier, but such claims call for empirical validation. We present a methodology for comparing concurrent languages for teaching purposes. A critical challenge is to avoid bias, especially when (as in our example application) the experimenters are also the designers of one of the approaches under comparison. For a study performed as part of a course, it is also essential to make sure that no student is penalized. The methodology addresses these concerns by using self-study material and applying an evaluation scheme that minimizes opportunities for subjective decisions. The example application compares two object-oriented concurrent languages: multithreaded Java and SCOOP. The results show an advantage for SCOOP even though the study participants had previous training in writing multithreaded Java programs. The lessons should be of use to educators interested in teaching concurrency, to researchers looking for objective ways of assessing teaching techniques, and to researchers who want to avoid bias in assessing an approach or tool that they have themselves designed.

The recent turn towards multicore processing architectures has made concurrency an important part of mainstream software development. As a result, an increasing number of developers have to learn to write concurrent programs, a task that is known to be hard even for the expert. Language designers are therefore working on languages that promise to make concurrent programming "easier". However, the claim that a new language is more usable than another cannot be supported by purely theoretical considerations, but calls for empirical studies. In this paper, we present the design of a study to compare concurrent programming languages with respect to comprehending and debugging existing programs and writing correct new programs. A critical challenge for such a study is avoiding the bias that might be introduced during the training phase and when interpreting participants' solutions. We address these issues by the use of self-study material and an evaluation scheme that exposes any subjective decisions of the corrector, or eliminates them altogether. We apply our design to a comparison of two object-oriented languages for concurrency, multithreaded Java and SCOOP (Simple Concurrent Object-Oriented Programming), in an academic setting. We obtain results in favor of SCOOP even though the study participants had previous training in writing multithreaded Java programs.

Software projects have crossed seas and continents looking for talented developers, moving from local developments to geographically distributed projects. This paper presents a case study analyzing the effect of distribution and time zones on communication in distributed projects. The study was performed in a university course during two semesters, where students developed projects jointly with teams located in ten different countries in South America, Europe, and Asia. The study compares the results of the projects distributed in two locations with projects distributed in three locations. It also analyzes projects in different time zone ranges. The initial results show that the amount of communication in projects distributed in two locations is bigger than the communication in projects distributed in three locations. We also found that projects in closer time zones have more communication than projects in farther time zones. Furthermore, we analyze the reply time for e-mails of projects distributed in different time zones, and discuss the challenges faced by the students during these projects.

Considerable progress has been made towards automatic support for one of the principal techniques available to enhance program reliability: equipping programs with extensive contracts. The results of current contract inference tools are still often unsatisfactory in practice, especially for programmers who already apply some kind of basic Design by Contract discipline, since the inferred contracts tend to be simple assertions - the very ones that programmers find easy to write. We present new, completely automatic inference techniques and a supporting tool, which take advantage of the presence of simple programmer-written contracts in the code to infer sophisticated assertions, involving for example implication and universal quantification.

Initial research in automated program fixing has generally limited itself to specific areas, such as data structure classes with carefully designed interfaces, and relied on simple approaches. To provide high-quality fix suggestions in a broad area of applicability, the present work relies on the presence of contracts in the code, and on the availability of static and dynamic analyses to gather evidence on the values taken by expressions derived from the code. The ideas have been built into the AutoFix-E2 automatic fix generator. Applications of AutoFix-E2 to general-purpose software, such as a library to manipulate documents, show that the approach provides an improvement over previous techniques, in particular purely model-based approaches.

Automated random testing has shown to be an effective approach to finding faults but still faces a major unsolved issue: how to generate test inputs diverse enough to find many faults and find them quickly. Stateful testing, the automated testing technique introduced in this article, generates new test cases that improve an existing test suite. The generated test cases are designed to violate the dynamically inferred contracts (invariants) characterizing the existing test suite. As a consequence, they are in a good position to detect new faults, and also to improve the accuracy of the inferred contracts by discovering those that are unsound. Experiments on 13 data structure classes totalling over 28,000 lines of code demonstrate the effectiveness of stateful testing in improving over the results of long sessions of random testing: stateful testing found 68.4% new faults and improved the accuracy of automatically inferred contracts to over 99%, with just a 7% time overhead.

Abstract Intuition suggests that random testing should exhibit a considerable difference in the number of faults detected by two different runs of equal duration. As a consequence, random testing would be rather unpredictable. This article first evaluates the variance over time of the number of faults detected by randomly testing object‐oriented software that is equipped with contracts. It presents the results of an empirical study based on 1215 h of randomly testing 27 Eiffel classes, each with 30 seeds of the random number generator. The analysis of over 6 million failures triggered during the experiments shows that therelative numberof faults detected by random testing over time is predictable, but that different runs of the random test case generator detectdifferent faults. The experiment also suggests that the random testing quickly finds faults: the first failure is likely to be triggered within 30 s. The second part of this article evaluates thenatureof the faults found by random testing. To this end, it first explains a fault classification scheme, which is also used to compare the faults found through random testing with those found through manual testing and with those found in field use of the software and recorded in user incident reports. The results of the comparisons show that each technique is good at uncovering different kinds of faults. None of the techniques subsumes any of the others; each brings distinct contributions. This supports a more general conclusion on comparisons between testing strategies: thenumberof detected faults is too coarse a criterion for such comparisons—thenatureof faults must also be considered. Copyright © 2009 John Wiley & Sons, Ltd.

Today's software projects are often distributed across multiple locations. This distribution poses new challenges produced by the cooperation across different countries, times zones, and cultures. Software engineering courses have to prepare students accordingly. This paper reports an experience on teaching a distributed software engineering course. In this course, students develop software in collaboration with five universities located in Italy, Hungary, Russia, Switzerland, and Ukraine. The projects allow students to face the difficulties of developing software in a globalized context, and provide a practical experience on distributed software engineering. We describe the major obstacles on organizing such a course, and we suggest best practices to achieve successful outcome.

A random testing strategy can be effective at finding faults, but may leave some routines entirely untested if it never gets to call them on objects satisfying their preconditions. This limitation is particularly frustrating if the object pool does contain some precondition-satisfying objects but the strategy, which selects objects at random, does not use them. The extension of random testing described in this article addresses the problem. Experimentally, the resulting strategy succeeds in testing 56% of the routines that the pure random strategy missed; it tests hard routines 3.6 times more often; although it misses some of the faults detected by the original strategy, it finds 9.5% more faults overall; and it causes negligible overhead.

Concurrency is an integral part of many robotics applications, due to the need for handling inherently parallel tasks such as motion control and sensor monitoring. Writing programs for this complex domain can be hard, in particular because of the difficulties of retaining a robust modular design. We propose to use SCOOP, an object-oriented programming model for concurrency which by construction is free of data races, therefore excluding a major class of concurrent programming errors. Synchronization requirements are expressed by waiting on routine preconditions, which turns out to provide a natural framework for implementing coordination requirements in robotics applications. As demonstration application, we describe a control program for hexapod locomotion, whose implementation closely follows the corresponding behavioral specification given by the biological model. We compare the architecture with solutions expressed in more traditional approaches to robotic control applications.

In program debugging, finding a failing run is only the first step; what about correcting the fault? Can we automate the second task as well as the first? The AutoFix-E tool automatically generates and validates fixes for software faults. The key insights behind AutoFix-E are to rely on contracts present in the software to ensure that the proposed fixes are semantically sound, and on state diagrams using an abstract notion of state based on the boolean queries of a class. Out of 42 faults found by an automatic testing tool in two widely used Eiffel libraries, AutoFix-E proposes successful fixes for 16 faults. Submitting some of these faults to experts shows that several of the proposed fixes are identical or close to fixes proposed by humans.

Developers write and execute ad-hoc tests as they implement software. While these tests reflect important insights of the developers (e.g., which parts of the software need testing and what inputs should be used), they are usually not persistent and are easily forgotten. They cannot always be re-executed automatically, for example to debug or to test for regressions. Several methods that make such test cases persistent and automatically executable have been proposed. They rely on capturing state and/or events at runtime and thus induce significant overhead or require specialized hardware. In previous work we proposed a method that, in the event of a failure, extracts test cases solely from the state at the time of the failure (and not from before the failure). We call this method "failure-state extraction". Capturing the state only at the moment of failure reduces the run-time overhead to zero, but comes at a cost: state extracted in this way cannot always be used to reproduce the failure. This paper provides an experimental evaluation of failure-state extraction. The results show that the method is highly effective: in the experiment, 90% of all failures were reproducible using failure-state extraction and thus could be extracted without run-time overhead.

Where do contracts - specification elements embedded in executable code - come from? To produce them, should we rely on the programmers, on automatic tools, or some combination?

Advances in recent years have made it possible in some cases to locate a bug (the source of a failure) automatically. But debugging is also about correcting bugs. Can tools do this automatically? The results reported in this paper, from the new PACHIKA tool, suggest that such a goal may be reachable. PACHIKA leverages differences in program behavior to generate program fixes directly. It automatically summarizes executions to object behavior models, determines differences between passing and failing runs, generates possible fixes, and assesses them via the regression test suite. Evaluated on the ASPECTJ bug history, PACHIKA generates a valid fix for 3 out of 18 crashing bugs; each fix pinpoints the bug location and passes the ASPECTJ test suite.

With the wide support for serialization in object-oriented programming languages, persistent objects have become common place. Retrieving previously ¿persisted¿ objects from classes whose schema changed is however difficult, and may lead to invalidating the consistency of the application. The ESCHER framework addresses this issues through an IDE-based approach that handles schema evolution by managing versions of the code and generating transformation functions automatically. The infrastructure also enforces class invariants to prevent the introduction of any corrupt objects. This article describes the principles behind invariant-safe schema evolution,and the design and implementation of the ESCHER system.

Abstract The SCOOP model extends the Eiffel programming language to provide support for concurrent programming. The model is based on the principles of Design by Contract. The semantics of contracts used in the original proposal (SCOOP_97) is not suitable for concurrent programming because it restricts parallelism and complicates reasoning about program correctness. This article outlines a new contract semantics which applies equally well in concurrent and sequential contexts and permits a flexible use of contracts for specifying the mutual rights and obligations of clients and suppliers while preserving the potential for parallelism. We argue that it is indeed a generalisation of the traditional correctness semantics. We also propose a proof technique for concurrent programs which supports proofs—similar to those for traditional non-concurrent programs—of partial correctness and loop termination in the presence of asynchrony.

The student project is a key component of a software engineering course. What exact goals should the project have, and how should the instructors focus it? While in most cases projects are artificially designed for the course, we use a deployable, realistic project. This paper presents the rationale for such an approach and assesses our experience with it, drawing on this experience to present guidelines for choosing the theme and scope of the project, selecting project tasks, switching student groups, specifying deliverables and grading scheme. It then expands the discussion to the special but exciting case of a project distributed between different universities, the academic approximation of globalized software development as practiced today by the software industry.

Intuition is often not a good guide to know which testing strategies will work best. There is no substitute for experimental analysis based on objective criteria: how many faults a strategy finds, and how fast. "Random" testing is an example of an idea that intuitively seems simplistic or even dumb, but when assessed through such criteria can yield better results than seemingly smarter strategies. The efficiency of random testing is improved if the generated inputs are evenly spread across the input domain. This is the idea of Adaptive Random Testing (ART).

Intuition suggests that random testing of object-oriented programs should exhibit a significant difference in the number of faults detected by two different runs of equal duration. As a consequence, random testing would be rather unpredictable. We evaluate the variance of the number of faults detected by random testing over time. We present the results of an empirical study that is based on 1215 hours of randomly testing 27 Eiffel classes, each with 30 seeds of the random number generator. Analyzing over 6 million failures triggered during the experiments, the study provides evidence that the relative number of faults detected by random testing over time is predictable but that different runs of the random test case generator detect different faults. The study also shows that random testing quickly finds faults: the first failure is likely to be triggered within 30 seconds.

The usual way to compare testing strategies, whether theoretically or empirically, is to compare the number of faults they detect. To ascertain definitely that a testing strategy is better than another, this is a rather coarse criterion: shouldn't the nature of faults matter as well as their number? The empirical study reported here confirms this conjecture. An analysis of faults detected in Eiffel libraries through three different techniques-random tests, manual tests, and user incident reports-shows that each is good at uncovering significantly different kinds of faults. None of the techniques subsumes any of the others, but each brings distinct contributions.

Ever growing expectations from students, university management and other stakeholders make course preparation increasingly time-consuming. Setting up a course from scratch requires producing many supporting documents such as syllabi, schedules, and course web sites listing the concepts being taught. This can be a considerable effort, taking time away from tasks with a more immediate pedagogical value, such as answering student questions and refining the concepts themselves.

Novices find it difficult to understand and use compiler error messages. It is useful to refine this observation and study the effect of different message styles on how well and quickly students identify errors in programs. For example, does an increased level of detail simplify the understanding of errors and their correction? We analyzed messages produced by a number of compilers for five programming languages, and grouped them into three style categories from their level of detail and presentation format, and correlated the level of experience and error type with performance and speed of response. The study involved two groups of students taking an introductory programming course at two different institutions; they used messages in these three styles to debug erroneous code. The results indicate that more detailed messages do not necessarily simplify the understanding of errors but that it matters more where information is placed and how it is structured.

Formally defining the knowledge units taught in a course helps instructors ensure a sound coverage of topics and provides an objective basis for comparing the content of two courses. The main issue is to list and define the course concepts, down to basic knowledge units. Ontology learning techniques can help partially automate the process by extracting information from existing materials such as slides and textbooks. The TrucStudio course planning tool, discussed in this article, provides such support and relies on Text2Onto to extract concepts from course material. We conducted experiments on two different programming courses to assess the quality of the results.

Progress in testing requires that we evaluate the effectiveness of testing strategies on the basis of hard experimental evidence, not just intuition or a priori arguments. Random testing, the use of randomly generated test data, is an example of a strategy that the literature often deprecates because of such preconceptions. This view is worth revisiting since random testing otherwise offers several attractive properties: simplicity of implementation, speed of execution, absence of human bias.

Curriculum and course planning is a key step in developing quality educational programs, but current practices very often lack a systematic approach. This article addresses this issue by refining and expanding the concept of Testable, Reusable Unit of Cognition (Truc). The methodology allows modeling courses and verifying compliance of a given course to a given description. It also makes it possible to describe precisely what students have previously learned and, as a result, adapt the teaching to their specific needs. The article presents a case study of comparing a subset of two introductory programming textbooks and describes the application TrucStudio that supports the methodology.

Randomized unit test cases can be very effective in detecting defects. In practice, however, failing test cases often comprise long sequences of method calls that are tiresome to reproduce and debug. We present a combination of static slicing and delta debugging that automatically minimizes the sequence of failure-inducing method calls. In a case study on the EiffelBase library, the strategy minimizes failing unit test cases on average by 96%.

One of the most difficult tasks in program verification is the "frame problem": guaranteeing that programs produce nothing more than their advertised effects. Even in a closed-world context, where the entire program is known, this is a delicate task especially in the presence of a modern programming language model with references and aliasing. As part of a general effort to verify the correctness of contract-equipped Eiffel software, involving proofs as part of a battery of verification techniques (along with others such as automatic contract-based testing), we are developing complementary approaches to mastering the frame problem, meant to be integrated in a practical proof workbench. One of these approaches relies on explicit specification of frame properties (modify/use); another infers these properties from a static analysis of the software. This is work in progress and the author reports directions of development and current advances rather than fully worked-out solutions or tools. The results include a systematic study of the aliasing phenomenon and point the way towards a general theory of object-oriented programming.

Although unit tests are recognized as an important tool in software development, programmers prefer to write code, rather than unit tests. Despite the emergence of tools like JUnit which automate part of the process, unit testing remains a time-consuming, resource-intensive, and not particularly appealing activity.This paper introduces a new development method, called Contract Driven Development. This development method is based on a novel mechanism that extracts test cases from failure-producing runs that the programmers trigger. It exploits actions that developers perform anyway as part of their normal process of writing code. Thus, it takes the task of writing unit tests off the developers' shoulders, while still taking advantage of their knowledge of the intended semantics and structure of the code. The approach is based on the presence of contracts in code, which act as the oracle of the test cases. The test cases are extracted completely automatically, are run in the background, and can easily be maintained over versions. The tool implementing this methodology is called Cdd and is available both in binary and in source form.

A program, or in object-oriented programming a feature, is characterized not only by an implementation but by a contract specifying its intent and a proof obligation to ascertain that the implementation meets the contract. From these ideas it is possible to derive a general framework for discussing programs and program development

Teaching introductory programming today presents considerable challenges, which traditional techniques do not properly address. Students start with a wide variety of backgrounds and prior computing experience; to retain their attention it is useful to provide graphical interfaces at the level set by video games; and with the ever-increasing presence of computing in society the stakes are higher, requiring a computing curriculum to introduce students early to the issues of large systems. We address these challenges through an "outside-in" approach, or "inverted curriculum", which emphasizes the reuse of existing components in an example domain involving graphics and multimedia, a gentle introduction to formal reasoning thanks to Design by Contract techniques, and an object-oriented method throughout. The new course has now been taught twice, with considerable gathering of student data and feedback; we report on this experience and its continuation.

While there's general agreement that the software engineering field is in great need of major advances, efforts are dispersed and not always directed to the really critical needs. I will present a view of what is fundamentally needed to produce real progress. The view is influenced by my own concerns and the talk is also an opportunity to present the research of my groups at ETH and Eiffel Software, with a special emphasis on: providing a basis for Trusted Components; certification of commercial components; realistic proofs of classes; advanced object-oriented techniques, making concurrent programming as simple as it should be; providing better tools; and management issues. Rather than emphasizing the fundable and fashionable, I will attempt to highlight topics that are truly important for our constituencies.

Reusable components equipped with strict guarantees of quality can help reestablish software development on a stronger footing, by taking advantage of the scaling effect of reuse to justify the extra effort of ensuring impeccable quality. This discussion examines work intended to help the concept of Trusted Component brings its full potential to the software industry, along two complementary directions: a "low road" leading to qualification of existing components, and a "high road" aimed at the production of components with fully proved correctness properties.

No abstract available.

article Free Access Share on Ensuring semantic integrity of reusable objects (panel) Authors: Webb Stacy View Profile , Richard Helm View Profile , Gail E. Kaiser View Profile , Bertrand Meyer View Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 27Issue 10Oct. 1992 pp 298–302https://doi.org/10.1145/141937.141961Online:31 October 1992Publication History 4citation292DownloadsMetricsTotal Citations4Total Downloads292Last 12 Months2Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Genericity, as in Ada or ML, and inheritance, as in object-oriented languages, are two alternative techniques for ensuring better extendibility, reusability, and compatibility of software components.This article is a comparative analysis of these two methods.It studies their similarities and differences and assesses to what extent each may be simulated in a language offering only the other.It shows what features are needed to successfully combine the two approaches in an object-oriented language that also features strong type checking.The discussion introduces the principal aspects of the language EiffePM whose design, resulting in part from this study, includes multiple inheritance and a limited form of genericity under full static typing. OVERVIEWDespite its name, today's software is usually not soft enough: adapting it to new uses turns out in most cases to be a harder endeavor than should be.It is thus essential to find ways of enhancing such software quality factors as extendibility (the ease

Abstract In a recent paper, a method was given for computing multidimensional sums in FORTRAN in a particular case. We show that the general problem of computing multidimensional sums is best expressed by a recursive definition which can then be translated into a programming language. The method is applied to an example optimization problem.