Welcome!

This website is associated with the course Contract Based Programming, e11. (Note that the course used to be called 'Contract Based Programming 2', but there is no associated '..1' course, and the name is currently being corrected in various contexts so you may see the '..2' in some places.) This site describes the contents of the course, the weekly schedule, and the projects, and it lists the participants and more. The leftmost part of each page in this website provides links to all the pages of the website.

About the Course

The objectives, contents, and method of the course are as follows.

Objectives

The objectives of the course is to learn how to systematically construct programs with contracts. After the course you will be able to read and write contracts in the shape of program assertions and class and method specifications based on predicate logic; you will be able to describe the relationship between the source code and associated program assertions such as contracts; and you will be able to use loop and class invariants and systematically construct the code and the associated assertions together.

Contents

This course covers specifications based on Hoare triples and predicate logic, the relation between specification and implementation, program assertions, validity, and correctness, the relationship between assertions and statements, loop invariants, class invariants, practical programming with contracts and assertions, and the relationship between assertions and testing.

Teaching format

It is a high priority of this course to create a good connection between the textbook material and the practical usage of the concepts and techniques introduced. In order to achieve this, every second week of the course is based on lectures, and the remaining weeks are practical projects done in groups.

There are 5 lectures each week in the weeks 44, 46, 48, and 50. The lectures will focus on material in the book and the lecture notes, as described on the 'materials' page. The intention of the lectures is to present and discuss the general concepts and principles, and to go through concrete examples of using them in the creation of proofs and contracts. It would be a good idea to read the relevant lecture notes and book chapters before the lecture, in order to be in a better position to ask about the difficult issues rather than starting from scratch. Material which has been presented earlier is expected to be known, but don't hesitate asking questions about it if something is unclear—that's much better than postponing it and letting unresolved issues add up over time.

During the remaining weeks, week 45, 47, and 49, there is project work in groups. The projects are intended to transform the general concepts and principles into concrete usage, and they also include some programming. In this context programming covers the production of traditional source code, but also annotating methods and classes with program assertions, and completing the software with some test cases. In all cases the project is documented by a report which must contain regular text explaining what has been done, and why.

An important reason for having projects in this course is that they should help establishing a robust connection between the abstract concepts and principles and some practical applications thereof, in order to make the resulting understanding deeper and more resilient. Hence, it is important to keep an eye on the connection between theory and practice at all times!

It is expected that project work takes about 15 hours per person per project.

Finally, note that the projects are used as a mandatory part of the course: In order to take the exam it is required that all 3 projects have been accepted by the teaching assistant.