Differences

This shows you the differences between two versions of the page.

--- course_outline [2011/02/10 22:37] – jonathan
+++ course_outline [2011/04/11 19:29] (current) – jonathan
@@ Line 68: / Line 68: @@
 **Tuesday's lecture:** We did the second refinement in the [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|ftp protocol]] in which we separate the sending and receiving agent. We had a lab session with Rodin, proving cross-products, powersets, relations and functions.
-**Thursday's lecture:** Third and final refinement in the [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|ftp protocol]] in which we add a parity bit. The distributed ftp protocol is now ready to be implemmented in code (how would you write the program?). Lab: prove the parity bit theorem.
+**Thursday's lecture:** Third and final refinement in the [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|ftp protocol]] in which 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.
 **Required Reading**: In the SVN==>Rodin folder, study: ''ref-card.pdf''
@@ Line 74: / Line 74: @@
 ===== Week 7 - February 14 =====
+**Tuesday's Lecture**: Did a manual proof of the theorem needed for the theory of parity (in the ftp protocol). This theorem was 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. We also did the initial model of the celebrity example (from the Exercises). We showed how to formalize the problem in Event-B using a "knows" relation. We dicussed the indentity and inverse relations and showed how the Celebrity axioms could be written in predicate logic or set theory. The celebrity example is one of the exercises that you must do in advance of Labtest1. [Challenge: In class we issued the following challenge: write a program given that takes as input a set of people and a knows relation, and outputs which person is the celebrity.
+**Thursday's lecture**: First Refinement of Celebrity. Then we start Chapter 15: Development of sequential programs. Binary search. Merging Rules.
+Celebrity example ideas: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations.
+**Required reading**: Chapter 15.
+**Exercises**: Up to an including Exercise 16.
@@ Line 110: / Line 120: @@
 Tuesday: Data refinement and Procedural Refinement. Illustration of these concepts using the Birthday Book example in which we write an initial specification, do a data refinement, followed by a procedural refinement; finally a merge produces code.
-Thursday: Labtest2
+BAG abstract datatype.
 ===== Week 12=====