The Calculus of Object Programs
Staff - Faculty of Informatics
Start date: 12 December 2011
End date: 13 December 2011
The Faculty of Informatics is pleased to announce a seminar given by Bertrand Meyer
DATE: Monday, December 12th, 2011
PLACE: USI Università della Svizzera italiana, room A13, Red building (Via G. Buffi 13)
It remains difficult to prove the correctness of object-oriented programs, especially when they manipulate complex data structures with references (pointers). I will present a theoretical framework for full correctness proofs, based on the combination of four ideas: compositional logic, a method for describing program semantics and proving program properties; negative variables to address the specifics of object-oriented programming, in particular qualified calls; the alias calculus, which determines whether reference expressions can ever have the same value, and handles the "frame problem" in this framework; and the calculus of object structures, a specification technique for the structures that arise during the execution of an object-oriented program. The running application is
the proof of correctness of a list reversal routine. A first draft of the approach is available in a technical report at http://se.ethz.ch/~meyer/publications/proofs/cop.pdf.
Bertrand Meyer is Professor of Software Engineering at ETH Zurich, the Swiss Federal Institute of Technology, research professor at ITMO (State University of Saint Petersburg) 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.
Other activities include: chair of the TOOLS conference series; director of the LASER summer school on software engineering; member, and chair since 2009, of the IFIP TC2 committee (Software technology); 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 doctorate from the Technical University (ITMO) of Saint Petersburg. Since 2011 he has been an adjunct research professor at ITMO, as holder of a newly created chair on Software Engineering and Verification.
HOST: Prof. Mauro Pezzè