Alessandra Russo's Software Engineering Course

These lecture notes are designed for the Master course Software Engineering, taught to master conversion students at Imperial College. This course is currently divided into two parts. The first part, taught by Emil Lupu is on systems modelling, design and analysis. Lecture notes are available from his home page. The second part is on formal specifications and the role that it plays in the software development process. It covers three main topics: (i) how to use formal languages, such as predicate logic, to write and reason about state-based formal specifications of software systems,(ii) how to extend such a formal language to allow for an object-oriented approach to formal specifications, and (iii) how to refine (object-oriented) formal specifications into object-oriented program specifications and use such specifications to reason about the correctness of (simple) object-oriented Java programs. The material for this second part of the course covers 12 hours lectures and 6 hours tutorials, and it includes one assessed tutorial.

Aims

The aims of this second part of the course are:

To provide an in-depth understanding of basic principles of (object-oriented) formal specifications of system requirements, and the skills and knowledge necessary to develop object-oriented specifications of computer-based systems.
To teach basic principles of (object-oriented) program specifications and their role in program verification and illustrate how they relate to (object-oriented) formal specifications of system requirements;

Learning Outcomes

Upon completion of these 12 lecture hours the students will have acquired an in-depth knowledge of fundamental principles of:

formal specifications (i.e. semantic issues, state and operation schemas, defensive versus non-defensive approach to specifications),

principles of and notations for specification and object orientation (i.e. class schema, visibility, class construct), techniques for specifying dependency and inheritance, usage of object-oriented specifications to prove system (safety) properties.

Finally, basic concepts of program specifications (i.e., techniques for specifying and reasoning about object-oriented programs) and relationships between formal specifications and program specifications, as well as a wide range of skills necessary for the design and specification of software systems.

Students will also be introduced to some existing tools when/where appropriate.

Prerequisites

This part of the course builds upon the first term courses:

Object Oriented Program Design.

Logic and AI Programming.

Books

The Way of Z, by J. Jacky, Cambridge University Press, 1997.
A good book that explains well (see first few chapters) what formal specifications are for.
Formal object-oriented specification using Object-Z, by Roger Duke and Gordon Rose, MacMillam Press Limited, 2000.
This book covers the part of our course on object-oriented formal specifications
Reasoned Programming., by Broda, Eisenbach, Khoshnevisan, and Vickers, Prentice Hall 1994.
This book covers the part of our course on reasoning about programs, as well as basic introduction to classical logic and formal reasoning.
Safeware: System Safety and Computers, by N. Leveson, Addison-Wesley, 1995
Software Engineering, by Ian Sommerville, Addison-Wesley, 2006.

Lecture Notes

Tutorials -->

Alessandra Russo

Course code: M225