Differences

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

--- course_outline [2012/02/15 03:49] – jonathan
+++ course_outline [2012/04/03 20:06] (current) – jonathan
@@ Line 38: / Line 38: @@
   * Controller events and Environment events
-===== Week 5 - Jan 31 =====
+===== FTP protocol =====
-This week we start Chapter 4 of the optional textbook -- A simple File Transfer Protocol (FTP). 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.
+Chapter 4 of the optional textbook -- A simple File Transfer Protocol (FTP).
+  * [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|ftp slides]]
-**Tuesday's lecture:** We reviewed the 2nd refinement question in Labtest1. We also did [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|ftp slides]] (up to slide 26). There are exercises you must do to review and extend your knowledge of sets, functions and relations.
+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.
-**Thursday's lecture**: We reviewed the first refinement of the ftp protocol. We then had a lab session in which the initial model and refeinement were entered in Rodin and proved. We also did some predicate logic in the theorem prover (with the aut-tactics disabled).
+In the second refinement in the [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|ftp protocol]] we did separate the sending and receiving agent. We had a lab session with Rodin, proving cross-products, powersets, relations and functions.
-**Required exercises this week** (not for marks): Do questions 5, 6, 7, 8 and 9 in //EventB-Questions.pdf// in the SVN.
+Third and final refinement 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.
+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.
-**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 questions 15 (celebrity.pdf) and 16 (ftp).
+**Exercises 11 and 12 in preparation for Labtest2**: Ex 11: ftp protocol. Ex12: Do the initial model of the celebrity example (from the Exercises). Formalize the problem in Event-B using a "knows" relation. Recall the indentity and inverse relations and show 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 Labtest2.
-===== Week 6 - February 7 =====
-**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.
+**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.
-**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''
-===== Week 7 - February 14 =====
+===== Sequential Programs =====
-**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.
+Requirements for the sorting algorithm. Initial specification using an anticipated event. First and second refinements leading to the use of merge rules for a loop within a loop. For the slides see [[http://deploy-eprints.ecs.soton.ac.uk/122/1/sld.ch15%2Cseq.pdf|Sequential Programs]].
-**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.
+Discussion. (a) 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. (b) BAG abstract datatype.
-**Required reading**: Chapter 15.
+In class we provided the following requirement:
-**Exercises**: Up to an including Exercise 16.
+REQ: Find an integer approximation to the square root of n.
+**Specification**
-===== Week 8=====
+  n,d: INT
-Finish 3rd refinement of ftp protocol [[http://deploy-eprints.ecs.soton.ac.uk/114/1/sld.ch4.file.pdf|slides]] from slide 44 to the end.
+  sqrt
+    require n >= 0
+    ensure (d^2 <= n < (d+1)^2) & (n = old n)
-Chapter XV: Development of sequential programs. Binary search. Merging Rules.
+Problem: Convert the above specification ito Rodin and use Rodin refinement rules to develop the code for the method //sqrt//.
-Celebrity example: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations.
+We did the celebrity problem ind detail including the addition of a variant for the new event and witnesses for disappearing parameters. We also studied injections, surjection and bijections of functions and relations. See Rodin folder.
-**Required reading**: all of chapter IV and chapter V (Event-B proof obligation rules).
-**Exercises**: Do exercise 11 (develop model, refinemenents and discharge proof obligations for ftp example).
-===== Week 9=====
-Event refinement proof obligation (from Hallersted-Event-B-Notation-2006.pdf in the SVN).
-Use of Add Hypothesis (AH) and Case analysis (DC) in the theorem prover. Use RichPoor example.
-Chapter XV: Development of sequential programs. Sort. Merging Rules.
-**Required reading**: chapter XV as covered in class and all of chapter IX (Mathematical Language).
-**Exercises**: Do exercise 12 (birthday book, data refinement, procedural refinement).
-===== Week 10=====
-Injections, surjections and bijections in Event-B.
-Requirements for the sorting algorithm. Initial specification using an anticipated event. First and second refinements leading to the use of merge rules for a loop within a loop. For the slides see [[http://deploy-eprints.ecs.soton.ac.uk/122/1/sld.ch15%2Cseq.pdf|Sequential Programs]].
-===== Week 11=====
+Review of arithmetic, set theory, predicate logic and Event-B invariant and refinement proof obligations. Translation between set theoretic statements and predicate logic. Re-write rules.
-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.
+===== Weakest Preconditions=====
-BAG abstract datatype.
+We did not cover weakest preconditions.
-===== Week 12=====
+Dijkstra weakest precondition calculus and loop variants and invariants.Proving loop termination. Relationship of Dijkstra weakest precondition calculus to Event-B. Slides on the SVN.
-Tuesday: Dijkstra weakest precondition calculus and loop variants and invariants.Proving loop termination. Relationship of Dijkstra weakest precondition calculus to Event-B. Slides on the SVN.
-Thursday: Review of arithmetic, set theory, predicate logic and Event-B invariant and refinement proof obligations. Translation between set theoretic statements and predicate logic. Re-write rules.
-===== Week 13=====
-Work through a complete example: requirements document, initial specification, refinements etc.