Differences

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

--- course_outline [2010/03/02 04:18] – 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).
-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=====
@@ Line 66: / Line 59: @@
 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).
@@ Line 75: / Line 70: @@
 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.
@@ Line 81: / Line 76: @@
 **Required reading**: chapter XV as covered in class and all of chapter IX (Mathematical Language).
-**Exercises**: Do execrcise 12 (birthday book, data refinement, procedural refinement).
+===== 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