Software Verification: Contracts, Trusted Components and Patterns
Bertrand Meyer, Manuel Oriol, Till Bay (Fall semester 2008)
| General info: | News | Course description | Grading | Course books | Downloads | Further reading | Exam | Wiki |
| Lectures: | Subjects and Slides |
General info
News
| 31.08.2008 | Website up and running, tentative schedule added. |
| 29.09.2008 | The exercises are available for Exercise Session 1. |
| 06.10.2008 | The exercises are available for Exercise Session 2. |
| 28.10.2008 | The project description is available. |
Course
description
Software Verification: Contracts, Trusted Components, and Patterns
Web page at the computer science department: 251-0239-00 (3G)
Trusted Components are reusable software elements accompanied with a guarantee of quality. They should be equipped with contracts describing their abstract properties. The course explores the various facets of this notion. Topics include: the notion of software quality; library design; the notion of design pattern, and whether patterns can be turned into components ("componentization"); program correctness and axiomatic semantics; testing; techniques of program analysis, model checking, abstract interpretation; proof-carrying code.
Grading
The project (a take-home exercise) will contribute 30% to the overall grade. A written exam on 15 December (during the usual lecture time) will contribute the remaining 70%.
Course
books
- Research articles may be required to read during the course.
- Eiffel Tutorial
- Bertrand Meyer: Object-Oriented Software Construction, Second Edition, Prentice Hall, 1997 ISBN 0-13-629155-4
- Robert V. Binder: Testing Object-Oriented Systems: Models, Patterns, and Tools, Addison-Wesley, 1999.
- Karine Arnout: From Patterns to Components, Ph.D. thesis, 2004. (See downloads)
- Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides: Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley, 1995, ISBN 0201634988
- Richard Mitchell, and Jim McKim: Design by Contract, by Example, Addison-Wesley, 2001, ISBN 0201634600
Downloads
- EiffelStudio 6.0 Free Edition is available for Windows, Linux, and MacOS. Click here!
- Arnout's Component library for Design Patterns. Click here!
Further
reading
About Eiffel and O-O programming:
- Karine Arnout: Eiffel: The Essentials, 2004 (Appendix A of Ph.D. dissertation From Patterns to Components).
- Peter Thomas, Ray Weedon: Object-Oriented Programming in Eiffel, Second Edition, Addison-Wesley Eiffel in Practice Series, ISBN 0-201-33131-4.
- Frieder Monninger: Eiffel. Objektorientiertes Programmieren in der Praxis, H. Heise Verlag, Hannover, ISBN 3-882-29028-5
- Bertrand Meyer: La produzione del software object oriented. Prentice Hall International, Hemel Hempstead, ISBN 88-256-0205-7
- Giuseppe Callegarin: Nuovo corso di informatica. Basi di dati e sistemi informativi. Per le Scuole superiori.CEDAM, ISBN 8-813-19565-6
- Karine Arnout's Ph.D. thesis: From Patterns to Components. Click here!
About Program Analysis:
- Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis, Springer, ISBN 3-540-65410-0.
- Neil D. Jones, Flemming Nielson: Abstract Interpretation: a Semantic-Based Tool for Program Analysis
Lectures
Stephan van Staden is the organizing assistant for the course. Please contact him if you have any questions. Schedule
Day |
Time |
Room |
| Monday | 9:00-11:00 | RZ F21 |
| Wednesday | 10:00-11:00 | RZ F21 |
Exam
Previous exams:
Week by Week Schedule