Eiffel at 25: Program
The slides of the talks can be accessed by clicking on the symbol next to each program item.
Wednesday, 24 November 2010
ETH Main Building (HG), Room F 33.1
9:00–10:30 Session 1
Session chair: Bertrand Meyer
- 25 Years of Eiffel IDEs: an Insider's Perspective
Emmanuel Stapf, Eiffel Software, U.S.A.
Like the Eiffel language, Eiffel tools have come a long way since the first
Eiffel-to-C compiler of 1986. EiffelStudio today is a modern multi-platform
IDE providing a wide array of facilities, some of them comparable to what
you find in competing tools (Eclipse, Visual Studio, ...), others still
off-the-wall (push-button automatic testing, text extraction from failed
cases, roundtrip engineering between text and diagrams, support for analysis
as well as design and programming, metrics tool etc.).
In unifying the Eiffel offering, EiffelStudio came out of a long line, or
rather tree, of developments. From the original "ec" compiler for Eiffel 1
to EiffelBench, EiffelCase, EiffelBuild and many others, some were kept,
some were subsumed by later developments, and some were dropped.
This talk presents the (so far) untold story of how Eiffel and EiffelStudio
came to fruition. It will walk you through the successful tools, the
challenges we had to tackle in building them, the sleepless nights spent
wondering whether the newest version would bootstrap, the ideas that were
retained and those that had to be dumped. It will explain the tight
relationship between the evolution paths of the language, the tools and the
supporting hardware and software platforms. It will not hide the mistakes
that were made along the way, but will explain how we recovered from them.
In the end it will, we hope, provide you with a clear understanding of why
and how Eiffel and EiffelStudio came to be what they are, and of their
contribution to the IT world.
- CloudStudio: Collaborative, Cloud-based Software Development
Martin Nordio, ETH Zurich, Switzerland
- A Modular Scheme for Deadlock Prevention in Eiffel's SCOOP
Scott West, ETH Zurich, Switzerland
10:30–11:00 Coffee break
11:00–13:00 Session 2
Session chair: Stephan van Staden
- Mathematical Modelling Languages in Eiffel
Jonathan Ostroff, York University, Canada
A specification is a precise description of the client's requirements. As
such, a specification is a contract between the client and the specifier as
well as between the specifier and the implementor. In specification
languages such as Z or B, the specification is one thing. The implementation
of the specification in an object oriented language such as Java or Eiffel
is something else, often leading to a certain amount of impedance mismatch
between the specification (in one notation) and the final implementation (in
an entirely different notation). Eiffel is designed with the single model
principle in mind, i.e. object oriented software is a single product that
supports multiple views. One view, suitable for compilation and execution,
is the full source code. Another view is a well-defined specification of
modules (or classes) amenable both to reuse and ultimately to formal
verification. All views work consistently within the same semantic context.
This talk describes the notion of model based contracts that extend classic
Design by Contract by means of expressive mathematical models of the kind
used in Z and B, but with the single model principle in mind. We show how
Eiffel's design simplicity and blend of powerful mechanisms such as strong
typing, agents, conversion, expanded as well as reference classes, void
safety, genericity and inheritance allow for the construction of model
specifications based on predicate logic and set theory. Executable model
based specifications can be used to document base libraries as well as
develop new software that use these libraries by first developing a
mathematical model and then refining the model into an implementation. The
use of the full Eiffel IDE with powerful debugging and testing capabilities,
UML diagramming and documentation facilities allow the implementation to be
validated using diverse systematic tests. However, we also discuss work
that has been done to verify the implementations using theorem proving.
- EiffelBase2: Strong Contracts for Design and Verification
Nadia Polikarpova, ETH Zurich, Switzerland
EiffelBase is, without any doubt, the most widely used Eiffel library.
Its data structures hierarchy is an excellent example of applying object-oriented techniques and Design by Contract.
However, there are known deficiencies in EiffelBase, the most important of which, in our opinion, is insufficient specification.
This talk presents EiffelBase2, a successor of EiffelBase, developed from the start with strong specifications and with the ultimate goal of proving its full functional correctness.
We will discuss model-based contracts:
a methodology to equip Eiffel classes with expressive and structures contracts,
and to evaluate the completeness of these contracts.
We will focus on how strong specifications solidify the design of the library, improve its usability and enable more extensive verification.
- Contracts and Testing, the Glamour of Eiffel Programming
Manuel Oriol, University of York, United Kingdom
- Automated Fixing of Programs with Contracts
Yi Wei, ETH Zurich, Switzerland
13:00–14:30 Lunch (Dozentenfoyer)
14:30–16:00 Session 3
Session chair: Martin Nordio
- Correctness by Construction: Developing High-integrity Systems
Piotr Nienaltowski, Altran Praxis, United Kingdom
Correctness by Construction is a radical and effective method of building high-integrity software systems, producing software with extremely low defect rates and achieving good productivity. It brings together four basic principles: rigorous requirements engineering, the use of formal methods, a systematic approach to system architecture, and static analysis.
The presentation will focus on that last principle: static analysis using SPARK. SPARK is a programming language and set of verification tools designed for the development of high-integrity systems. It relies on Design by Contract, information flow analysis, verification-condition generation and theorem proving to achieve fully static verification of software. The presentation will cover the design goals of SPARK, its major features, the various forms of analysis provided by the tools, and some examples of industrial SPARK projects in aerospace, rail and government security.
The primary goal of the language – static verifiability of software – leads to challenging trade-offs in the design. I will discuss these trade-offs and cover some interesting differences between SPARK and Eiffel, including the design of the contract language and state abstraction.
- A Verification Assistant for Eiffel Programs
Julian Tschannen, ETH Zurich, Switzerland
- Contracts for Verification – a Personal Perspective
Carlo A. Furia, ETH Zurich, Switzerland
16:00–16:30 Coffee break
16:30–18:00 Session 4
Session chair: Sebastian Nanz
- Applying Eiffel to Large-scale Developments in Business Information Systems
Paul-Georges Crismer, Groupe S, Belgium
- Diverse Uses of Eiffel in Industry, and Thoughts for the Future
Thomas Beale, Ocean Informatics, United Kingdom
- Perspectives for the Evolution of Eiffel
Bertrand Meyer, ETH Zurich, Switzerland