The Taub Faculty of Computer Science Events and Talks

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