course_outline
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
course_outline [2010/02/22 01:56] – jonathan | course_outline [2010/03/04 04:57] (current) – jonathan | ||
---|---|---|---|
Line 53: | Line 53: | ||
===== Feb 15: reading week ===== | ===== Feb 15: reading week ===== | ||
- | ===== Week 8: Feb 22===== | ||
- | Discussion of Assignment 3 (celebrity). | + | ===== Week 9: Feb 22===== |
- | Chapter XV: Development of sequential programs. Binary search. Sorting. Merging Rules. | + | Chapter XV: Development of sequential programs. Binary search. Merging Rules. |
- | **Required reading**: chapter XV as covered in class and and chapter V (Event-B | + | Celebrity example: Relations, functions, identity relation, inverse. Feasibility |
- | ===== Week 9: Feb 22===== | + | 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**: | ||
+ | |||
+ | ===== 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/ | ||
+ | |||
+ | Dijkstra [[http:// | ||
- | **Required reading**: all of chapter IX (Mathematical Language). | + | Chapter XVI: Location access controller |
course_outline.1266803800.txt.gz · Last modified: 2010/02/22 01:56 by jonathan