course_outline
Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
| course_outline [2010/03/02 04:18] – jonathan | course_outline [2010/03/02 04:21] – jonathan | ||
|---|---|---|---|
| Line 53: | Line 53: | ||
| ===== Feb 15: reading week ===== | ===== Feb 15: reading week ===== | ||
| - | ===== Week 8: Feb 22===== | ||
| - | |||
| - | Discussion of Assignment 3 (celebrity). | ||
| - | |||
| - | Chapter XV: Development of sequential programs. Binary search. Merging Rules. | ||
| - | |||
| - | **Required reading**: chapter XV as covered in class and and chapter V (Event-B proof obligation rules). | ||
| ===== Week 9: Feb 22===== | ===== Week 9: Feb 22===== | ||
| Line 66: | Line 59: | ||
| Celebrity example: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, | Celebrity example: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, | ||
| + | |||
| + | 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). | **Required reading**: all of chapter IV and chapter V (Event-B proof obligation rules). | ||
| Line 75: | Line 70: | ||
| Event refinement proof obligation (from Hallersted-Event-B-Notation-2006.pdf in the SVN). | 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. | + | How an anticipated event helps to specify termination. |
| Chapter XV: Development of sequential programs. Sort. Merging Rules. | Chapter XV: Development of sequential programs. Sort. Merging Rules. | ||
| Line 81: | Line 76: | ||
| **Required reading**: chapter XV as covered in class and all of chapter IX (Mathematical Language). | **Required reading**: chapter XV as covered in class and all of chapter IX (Mathematical Language). | ||
| - | **Exercises**: | ||
| + | ===== Week 10: March 8===== | ||
| + | |||
| + | Chapter XVI: Location access controller | ||
course_outline.txt · Last modified: 2010/03/04 04:57 by jonathan