Robust Programming

This course will present foundational techniques for reasoning about the behaviour of object-oriented and imperative programs. Students will learn how these techniques can be employed during the design phase or at later stages of development. In particular, they will see how semantics can be formally defined and how static checking works, and will be introduced to the design-by-contract approach.

Course dates

Objectives

After attending the course, the students will understand:

• ways of thinking about semantics of programs;
• how assertions can help debugging and writing better code;
• how to identify loop invariants;
• how to “prove” correctness of programs using Hoare logic;
• basic concepts and advantages of the design-by-contract approach;
• capabilities of state-of-the-art static analysis tools. In broader terms, this knowledge will help students understand how to break programming tasks into smaller pieces and reason about them, or how to improve their code testing.

Contents

• Runtime assertion checking: pros and cons of runtime checking and testing.
• Writing useful assertions: preconditions and postconditions, invariants, weakest preconditions and strongest postconditions.
• Static checking: common approaches and main challenges (undecidability, state-space explosion), tools and their capabilities.
• Design by contract: use for development, testing, generating documentation and for static checking; abstraction and refinement of contracts.
• Operational semantics: giving formal meaning to imperative programs.
• Hoare logic for simple imperative programs: partial correctness, total correctness. Extending Hoare logic to more complex data types: brief introduction to separation logic.

Requirements

The students should have a working knowledge of an object oriented programming language (ideally C# or Java). The practicals will be mainly done in C#, and hence it is recommended that students not familiar with it learn its basic syntax before the teaching week, for example by solving exercises given as part of the prestudy. Further, students should know the basics of set theory and propositional logic, for example gained by attending SEM.