A Course on Correctness by Construction

Motivation and Goals

Software is becoming increasingly complex and responsible for critical tasks. Any technology aimed at ensuring the reliability and quality of software will be increasingly relevant, if not utterly necessary.

Only rigorous (e.g., mathematically sound) approaches can certify software with the highest possible assurance. These approaches include, among others, the use of specification languages, high-level programming languages (including equational, functional, and logic languages), the use of model checking and deductive verification, language-based approaches often interacting with theorem provers.

In this course we will give a hands-on introduction to rigorous software development methods that follow a “correctness-by-construction” approach.

While the course is not heavy in theory, everyone is expected to have a good understanding of first-order logic and programming experience. We will explore several methodologies that have approaches and underlying technical bases, but which share a common overarching goal: develop programs while making sure that non-trivial properties, expressing high-level design requirements regarding correctness, fairness and sometimes efficiency, are continuously respected.

OR-Left

To follow this course, you should have programming experience (three years or more), familiarity with formal (first-order) logic, formal proofs, logic programming, and concurrent programming. If you think you do not meet these requirements, please get in touch ASAP with one instructor to recommend you reading material.

Course Log and Pointers to Class Material

Click on the dates to expand the lecture’s content.

02/2/2022: General Introduction (Click on me!)

General motivation (slides) and the beginning of an introduction to Event-B (slides).

First Part: System Modelling using Refinement and Interactive Theorem Proving

09/02/2022: More on Event-B.

We continued with the introduction to Event-B: Events, constants, axioms, variables, guards, invariants. Quick review of syntax of propositional logic and inference rules.

16/02/2022: Inference rules, correctness, proofs by contradiction, intro to Rodin.

We finished reviewing the inference rules for propositional logic and continued with the correctness proofs for the integer division algorithm — by hand. We also made some remarks on why a “proof by contradiction” is admissible. We started using Rodin: we proved the correctness of the integer division model and started working on the search in an array.

Find here the slides for the first and the second parts and the recording of the edition in Rodin.

23/02/2022: Using Rodin to refine models.

We continued with Rodin, refining the search model that does a random search. We model a linear search and prove it is a correct refinement and termination. We also start the development of binary search refining the random search model. Slides here and the recording of the actual work with Rodin.

02/03/2022: Correctness of refinement and interactive proofs

Using as running example the search in a sorted array we have seen what are, formally, the correctness conditions for a refinement and applied them to the correctness and termination of the search in an array. We used Rodin to interact with the provers and had a hands-on session on how to deal with non-trivial proofs. The slides are available here. The recording of the interaction with the tool is here. A video with more details on the interaction with the theorem provers is also available.

09/03/2022: No lecture today – ETSIINF follows a Monday schedule.

$\emptyset$

16/03/2022: Review of homework. First model of the cars over a one-way bridge.

We reviewed the homework and finished the binary search example with some reflections on having theorems deduced from the axioms and, for the particular case of the binary search, how well-definedness plays a role in writing implications and transforming them in contrapositions. The slides are here. We started as well our next example and we wrote the initial model of a controller for cars that travel over a narrow bridge.

23/03/2022: Clarification of homework. First refinement of the “narrow bridge” problem.

We finished the first refinement of the cars in a narrow bridge problem. Slides here, a video of the edition of the models here, and the model so far is here.

30/03/2022: Second refinenement of the “narrow bridge” problem.

We introduced the traffic lights and modeled the behavior of the systems paying special attention to its correctness. Several invariants expressing safety conditions were introduced. Last, some considerations regarding liveness were made. The slides are here, the model with the second refinement is here, and the video with the interactions with Rodin made during the lecture is here. A video with the proof of the absence of deadlock is here.

06/04/2022: Controllers and environment. Data structures.

We finished the narrow bridge problem by refining the model and introducing the sensors, splitting the model between logic and environment simulation. The slides are here and the full model is here. We also described how to model simple data structures in Rodin and we derived a scheme for infinite well-founded induction.

13/04/2022: No lecture today: Easter Holidays.

20/04/2022: Predicate logic, sets, relations, functions. Intro to a distributed system model.

We reviewed the basics of predicate calculus, focusing on the meaning of the quantifiers, equivalences, and inference rules. We summarily reviewed sets, how they are used to construct relations, and how a specific class of relations are functions. Slides here. We also started the development of a distributed system.

27/04/2022: Synchronization of a distributed system

We continued with the definition of a distributed system. The slides used so far are here and the Rodin model is here.

4/05/2022: Synchronization of a distributed system

We finish our example of a synchronized distributed system by modeling the downwards wave, proving it correct, and making changes so that it can run forever in constant space. Slides here. The proof of invariant 3 preservation by ascending in model 4 is here. The proof of guard strengthening in descending_nr (model 4, again) is here. The full model, with all the proofs, is here.

11/5/2021: A COVID-compliant market and some animation and model checking.

Today we presented the design and development of a market that works following some (partially imaginary) rules for COVID. As usual, you can find the slides, the full model, and video with a short session of animation plus model checking (because there was some PO that should be immediate to discharge, but something wrong prevented me from being able to do it).

18/5/2021: No lecture today – free time because of the session next week.

Project Presentation Sessions

We plan one or two presentation sessions. We may have to use additional sessions depending on the number of project teams.

25/05/2022: Presentations (tentative)

08/06/2022: Regular exam date

This date is only available for those that at the beginning of the course chose to go to a final exam instead of a continuous evaluation.

08/07/2022: Extraordinary exam (resit)


Location, Schedule, Administrivia

Place and time

During the academic year 2021-2022 we will meet physically at classroom 6306 from 4pm to 7pm on Wednesdays. We will post any exception on the course mailing list (see below) and the course log.

Teachers

Manuel Carro (coordinator)

Office 035 at the IMDEA Software Institute (under appointment)- mcarro |at| fi DOT upm DOT es.

Manuel Hermenegildo

Office 386 at the IMDEA Software Institute (under appointment) – herme |at| fi DOT upm DOT es.

Communication

The mailing list archives are at https://software.imdea.org/mailman/private/cbc/ .

For security reasons, you cannot subscribe to the mailing list by yourself. You should have been subscribed by some instructor, and you should have received a welcome message with the initial subscription. Note that you can only post to the list from the mail address that has been subscribed. If you want to change it, please let an instructor know. In normal situations, all important classroom announcements will go through the course mailing list, so please be sure to read the subscribed address regularly.


Course Policy

To keep this landing page short, the course policy appears in a separate page. This does not mean it is less important. Please make sure to read it.


Academic Resources

Please have a look as well at the Assorted Resources. It contains not-strictly-academic (but interesting) material!

Logic

  • Lawrence Paulson’s Logic and Proof are the course notes of the author for a Logic course in Cambridge. Highly recommended, as they are both rigorous and very concise. They provide very good background material for both parts of the course.
  • A very good book on the use of logic in computer science is Logic in Computer Science, by Huth and Ryan. It seems to be out of print, but the Computer Science School should have several copies. You may also consider locating an electronic copy on the Internet, if possible of the second edition.
  • Mathematical Logic for Computer Science. Mordechai Ben-Ari. There should be copies in the School’s library.
  • Sweet Reason: a Field Guide to Modern Logic.  James M. Henle, Jay L. Garfield, Thomas Tymoczko. This book explains several topics on logic and logic reasoning with many entertaining non-technical examples from many sources. It does not focus on logic and computation, however.
  • Class notes on Gentzen systems and single-conclusioned Gentzen systems and refinement logic (the sequent calculus we use in the lectures) from the Spring 2009 CS 4860 (Applied Logic) course in Cornell. Syntax node: these classnotes sometimes use “⊃” to denote implication, when we (and many others) use “⇒”.

Formal Development

  • Faultless Systems: Yes, we Can! is a short article by Jean-Raymond Abrial, the creator of Event-B (among other systems and proposals for rigorous software development) that explains the ideas behind the Event-B methodology.
  • Twenty-Five Years of the B-Method: a short overview of the history of B and its descendant Event B and some of the projects in which it has been used.

Event B Reference

  • The definitive reference for Event B is Modeling in Event-B: System and Software Engineering, by Jean-Raymond Abrial.
  • The richest information point for Event B is the Event B wiki. A summary of the inference and equality rules, axioms, proof obligations, and syntax of Event B can be found in these slides.
  • This reference card has a (very useful) summary of the Event B notation.
  • The mathematical toolkit of Event B is explained in a report.
  • An introduction to the Event-B method with a description of its phases.

Tools

Rodin

The essential tool to perform development with Event B is Rodin, an Eclipse-based tool. It includes an editor for the components of an Event B project that keeps track of the pending proof obligations and tries to discharge them on the fly. It has many plugins (installable directly from Rodin) that provide advanced theorem proving capabilities (to discharge proof obligations on demand and, hopefully, with only a button press), model checkers, animation, printout generation, and much more. You need to install it, as it will be use extensively during the course.

Please read this quick guide to installing Rodin. It includes some tips and instructions to perform several common tasks. This will save you time! At point, you will need to interact with the theorem provers. A page with tips for proving will be handy!

  • Homepage of the Rodin versions. Please make sure to download the latest version.
  • Installation instructions for RODIN.
  • The handbook for Rodin. It does not correspond the latest tool version: some details differ, but the basic ideas remain.
  • The Atelier B Provers plugin is necessary for any non-trivial development. Install it by going to Help ⇒ Install new software ⇒ select Atelier B Provers ⇒ Select in box ⇒ Click Next ⇒ Follow instructions. If you do not install these provers, many course examples will not work.
  • Relevant sections of the manuals:
    • How to set up a Rodin project (we will see it during the lectures).
    • Hints on discharging proofs using RODIN. Read it: it contains many hints and information on how to use the built-in and external theorem provers.
    • An explanation of the proving perspective from the user interface point of view.
    • A catalog of the proof obligations generated by RODIN and their meaning.
  • A list of the inference rules and rewriting rules in the default Event B prover (extracted from the Event B website).

Ciao

During the second part of the course you will run the examples and exercises discussed in class on Ciao, a programming system in the Prolog family which allows using pure logic programming, standard Prolog, functions, constraints, and several other paradigms and language extensions.

The following are useful resources for Ciao:

This technical paper provides a good overall overview of the system as well as the motivations behind Ciao’s design.