CSE6411

User Tools

Site Tools

You are here: CSE6411-W10 » Course Outline
Trace:
course_outline

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
course_outline [2010/01/29 20:33] – jonathancourse_outline [2010/03/04 04:57] (current) – jonathan
Line 37: Line 37:
 **Required exercises this week** (not for marks): Do questions 3, 4 and 5 in (see //EventB-Questions.pdf// in the SVN). Also, use Rodin to prove the bridge controller up to the second refinement (done in in class). **Required exercises this week** (not for marks): Do questions 3, 4 and 5 in (see //EventB-Questions.pdf// in the SVN). Also, use Rodin to prove the bridge controller up to the second refinement (done in in class).
  
-**Required Readings**: Textbook, Chapter II, up to p45+**Required Readings**: Textbook, Complete Chapter II on your own.
  
 ===== Week 5: Feb 1 ===== ===== Week 5: Feb 1 =====
 +
 +This week we do Chapter IV of the textbook – A simple File Transfer Protocol (FTP). There are exercises you must do to review and extend your knowledge of sets, functions and relations. 
  
 **Required exercises this week** (not for marks): Do questions 7, 8 and 9 in (see //EventB-Questions.pdf// in the SVN). Also, use Rodin to prove the bridge controller up to the second refinement (done in in class). Questions 8 and 9 will develop your ability to use functions and relations which is required for the rest of the course. **Required exercises this week** (not for marks): Do questions 7, 8 and 9 in (see //EventB-Questions.pdf// in the SVN). Also, use Rodin to prove the bridge controller up to the second refinement (done in in class). Questions 8 and 9 will develop your ability to use functions and relations which is required for the rest of the course.
Line 45: Line 47:
 ===== Week 6: Feb 8 ===== ===== Week 6: Feb 8 =====
  
 +Finish up to and including 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. 
 +
 +**Required reading**: all of chapter IV 
 +
 +===== Feb 15: reading week =====
 +
 +
 +===== Week 9: Feb 22=====
 +
 +Chapter XV: Development of sequential programs. Binary search. Merging Rules.
 +
 +Celebrity example: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations.
 +
 +Use of Add Hypothesis (AH) and Case analysis (DC) in the theorem prover. Use RichPoor example.
 +
 +**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: March 1=====
 +
 +Event refinement proof obligation (from Hallersted-Event-B-Notation-2006.pdf in the SVN).
 +
 +How an anticipated event helps to specify termination.
 +
 +Chapter XV: Development of sequential programs. Sort. Merging Rules.
 +
 +**Required reading**: chapter XV as covered in class and all of chapter IX (Mathematical Language).
 +
 +
 +===== Week 10: March 8=====
 +
 +Complete the refinement/proof of the sort program.
 +
 +Dijkstra [[http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD472.PDF|guarded command language]] and proofs of loops via variants and invariants.
 +
 +Chapter XVI: Location access controller
course_outline.1264797201.txt.gz · Last modified: 2010/01/29 20:33 by jonathan