The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed:

Use this small project to get started with Event-B and the Rodin tool

• Simple Bank System. Introduction to Specification and Refinement.
• Video Presentation

* Read the Rodin Users handbook up to and including Section 2.5.2.

• Bridge controller (reactive systems) Chapter 2: Controlling cars on a bridge).
• Required readings: Read Chapters 1 and 2 from the suggested text chapter 2

Topics covered by the bridge controller include

• Initial models and Proof rules for invariant preservation
• Refinement/correct by construction
• Proof rules for refinement
• Deadlock prevention and relative deadlock
• Divergence, Convergent events and variants
• Proof rules including SIM
• Controller events and Environment events

Chapter 4 of textbook – A simple File Transfer Protocol (FTP).

• ftp slides

In the previous example, the program was reactive (i.e. it had to control an external situation such as cars on a bridge). This chapter deals with a protocol used on a computer network to transfer data from a sender to a receiver. The example will also allow us to extend our mathematical language with sets, functions and relations. As usual we will start with a requirements document. The initial model tells us what the protocol is supposed to achieve without telling us how to achieve it; how to achieve it will be dealt with in succesive refinements. Note that the model presented in the slides (using the notion of an anticipated event) is different than that of the textbook.

In the second refinement in the ftp protocol we separate the sending and receiving agent.

In the third and final refinement we add a parity bit. The distributed ftp protocol is now ready to be implemented in code (how would you write the program?) with a guarantee that it will terminate with the file properly transmitted from the sender to the receiver. Lab: prove the parity bit theorem.

Try a manual proof of the theorem needed for the theory of parity (in the ftp protocol). This theorem might be hard to prove. The suggestion is to first do the proof manually, which then makes it easier to do in Rodin. Using this approach, we were able to derive a Lemma that was helpful in the Rodin proof.

Do all the lab exercises in preparation for the latest Required reading**: all of chapter IV and chapter V (Event-B proof obligation rules). Injections, surjections and bijections in Event-B. Review: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations.

Sequential Programs. This is Chapter 15 in the text (which is required reading). This includes the merging rules.

We study two examples of the development of programs using loops by Dijkstra using the Hoare notation and the proof obligations for loop invariants and variants. Separation of concerns via partial correctness and termination arguments. Weakest preconditions and the wp-axiom for assignment. See also the slides “LoopsAndDisjkstra”. This topic is dicussed in detail in Science of Programming (David Gries, chapter 11).

See slides 10. Hoare logic, program verification and and Dijkstra's urn problem.

C.A.R Hoare won the Turing Award in 1980. “Hoare made two bold additional steps, and his “An axiomatic basis for computer programming” is one of the most influential papers on the theory of programming. First he discarded the flowcharts and developed a logical system for reasoning about programs using specifications of statement behavior that have become known as Hoare triples. Secondly, he argued that his “axiomatic” system could be viewed as an abstract way of recording the semantics of programming languages.

The first of these steps has the profound effect of opening up a way of developing provable programs rather than treating their verification as a post hoc concern. Hoare published a number of developments of this idea, and the pursuit of “Hoare semantics“ has had a profound effect on the understanding of programming languages and the task of reasoning about programs. There is a fascinating link back to work by Alan Turing in the late 1940s.

• Turing Award 1980
• Award Speech about Hoare Logic

TLA Videos

See slides 11: Thinking for Programmers. Leslie Lamport's TLA+ specification tool, its use at Amazon and for MS/Xbox 360. Thinking for programmers. QuickSort at the algorithmic level as a divide and conquer algorithm rather than a program. The algorithm can be refined to a recursive implementation, an iterative implementation and a concurrent implementation.

• Lamport's Talk
• Lampsort as an algorithm in Eiffel
• Leslie Lamport won the 2013 Turing award for: For fundamental contributions to the theory and practice of distributed and concurrent systems, notably the invention of concepts such as causality and logical clocks, safety and liveness, replicated state machines, and sequential consistency. here.

See slides 12. Method for systematic development correct-by-construction reactive systems.

The following examples are unlikely to be on the exam.

Develop a phone book example by developing a mathematical model from informal E/R-descriptions. Relations, Functions and the override operator, relational image, relational inverse, domain and range restrictions and subtractions, and relational composition.

Develop an Event-B project for an EHealth medication system.

For the EHealth system the requirements were:

• E1: a set of doctors prescribes drugs to a set of patients
• E2: there exists pairs of drugs that when taken together have undesirable interactions
• E3: Drug interaction is symmetric, i.e. if a drug interacts with another, then the reverse also applies
• R1: A doctor shall be capable of adding drugs to a patients’ prescription.
• R2: A doctor shall not prescribe two drugs that interact
• Goal: minimize the number of undesirable interactions