Differences

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

--- course_outline [2010/03/02 04:17] – jonathan
+++ course_outline [2010/03/04 04:57] (current) – jonathan
@@ Line 53: / Line 53: @@
 ===== 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. Merging Rules.
-**Required reading**: chapter XV as covered in class and and chapter V (Event-B proof obligation 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.
-===== 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**: 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.
-**Required reading**: all of chapter IX (Mathematical Language).
+Chapter XVI: Location access controller