Time+Place: Monday 20/02/2017 14:30 Room 337 Taub Bld.
Title: Class invariants: old concept and new results
Speaker: Bertrand Meyer - GUEST LECTURE - Note unusual day http://se.ethz.ch/~meyer/
Affiliation: Professor of Software Engineering, ETH Zurich
Host: David H. Lorenz

Abstract:


Class invariants play a central role in understanding
object-oriented programming. They also raise some
tricky problems for the verification of OO programs, in
particular "furtive access", resulting from callbacks,
and "reference leak", a consequence of aliasing.

I will start with a tutorial on class invariants,
explaining why OO programmers should understand the
concept (although today many do not even know that it
exists). Then I will describe the verification issues,
which have attracted a considerable amount of research,
and present my own recent results which, I hope,
provide the solution. They take the form of three rules:
the O-rule, a general Hoare-style inference rule for
object-oriented programming (surprisingly, until now
no widely accepted rule exists); the export consistency
rule, a simple sanity condition complementing standard
information-hiding properties; and the inhibition rule,
taking care of reference leak. The talk includes several
examples, such as the Observer pattern and linked
structures, which have proved difficult to handle in
previous approaches, and shows how the rules handle
them. A distinctive property of the approach is that
it uses no new language construct and no new programmer
annotations whatsoever.

The talk explains all the concepts it uses; it
is accessible to anyone with basic experience of
object-oriented programming.
 

Short Bio:
==========

Bertrand Meyer is Professor of Software Engineering at
ETH Zurich, the Swiss Federal Institute of Technology,
research professor at Innopolis University (Kazan,
Russia) and Chief Architect of Eiffel Software (based
in California).

He is the initial designer of the Eiffel method and
language and has continued to participate in its
evolution. He also directed the development of the
EiffelStudio environment, compiler, tools and libraries
through their successive versions.

His latest two books (both published by Springer)
are: Agile! The Good, the Hype and the Ugly (2014),
a presentation and critical analysis of agile methods;
and  Touch of Class: Learning to Program Well, Using
Object Technology and Contracts (2009), an introductory
programming textbook based on several years of teaching
introductory programming at ETH (see Amazon page and
Springer page).

Earlier books include Object-Oriented Software
Construction, (a general presentation of object
technology, winner of the Jolt Award); Eiffel: The
Language, (description of the Eiffel language); Object
Success (a discussion of object technology for managers);
Reusable Software (a discussion of reuse issues and
solutions);  Introduction to the Theory of Programming
Languages. He has also authored numerous articles (see
publication list) and edited or co-edited several dozen
conference proceedings, including  the 2005 "Verified
Software".

Other activities include: chair of the TOOLS conference
series ; director of the LASER summer school on software
engineering (taking place every year since 2004 in
early September in Elba island, Italy); member of
the IFIP Working Group 2.3 on Programming Methodology;
member of the French Academy of Technologies. He is also
active as a consultant (object-oriented system design,
architectural reviews, technology assessment, patents and
software litigation), trainer in object technology and
other software topics, and conference speaker. Awards
include ACM Software System Award, Fellow of the ACM,
Dahl-Nygaard Prize, Harlan D. Mills Prize, and honorary
doctorates from the University of York in the UK and the
Technical University (ITMO) in Saint Petersburg.

Prior to founding Eiffel Software in 1985, Meyer had
a 9-year technical and managerial career at EDF, and
was for three years on the faculty at the University
of California. His experience with object technology
through the Simula language, as well as early work on
abstract data types and formal specification (including
participation in the first versions of the Z specification
language) provided some of the background for the
development of Eiffel.

At ETH Zurich and ITMO he pursues research on the
construction of high-quality software (see Web site of
the ETH Chair of Software Engineering).
 
==========================================
Refreshments will be served from 14:15
Lecture starts at 14:30