Differences

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

--- course_outline [2011/02/06 03:37] – jonathan
+++ course_outline [2011/04/11 19:29] (current) – jonathan
@@ Line 62: / Line 62: @@
 **Required Reading:** See SVN (folder ''04-ftp''): Read ''04-ftp.pdf'' and ''05-eventb-notation.pdf''.
-**Note**: Labtest2 is on March 1. By that time you must finish up to and inluding question 15 (celebrity.pdf).
+**Note**: Labtest2 is on March 1. By that time you must finish up to and inluding questions 15 (celebrity.pdf) and 16 (ftp).
-===== Week 6 - Febbruary 7 =====
+===== Week 6 - February 7 =====
-**Tuesday**: Second and Third refinemnets of the [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|ftp]] protocol.
+**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.
-We also use sets and functions to model a banking system using Rodin (in class).
+**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''
-===== Reading week =====
+===== 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.
-Work on Assignment 2
 ===== Week 8=====
@@ 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=====