Differences

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

--- course_outline [2010/03/02 04:12] – jonathan
+++ course_outline [2010/03/25 20:56] (current) – jonathan
@@ Line 65: / Line 65: @@
 Chapter XV: Development of sequential programs. Binary search. Merging Rules.
-Celebrity example: Relations, functions, identity relation, inverse. Refinements, convergence and proof obligations.
+Celebrity example: Relations, functions, identity relation, inverse. Feasibility proof obligations for non-deterministic assignment, witness (WITH) for local variable refinements, convergence and proof obligations.
 **Required reading**: all of chapter IV and chapter V (Event-B proof obligation rules).
@@ Line 72: / Line 72: @@
 ===== Week 9: March 1=====
+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.
@@ Line 79: / Line 81: @@
 **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).
+**Exercises**: Do exercise 12 (birthday book, data refinement, procedural refinement).
+===== Week 10: March 8=====
+Injections, surjections and bijections in Event-B.
+Requirements for the sorting algorithm. Initial specification using an anticipated event. First and second refinements leading to the use of merge rules for a loop within a loop. For the slides see [[http://deploy-eprints.ecs.soton.ac.uk/122/1/sld.ch15%2Cseq.pdf|Sequential Programs]].
+===== Week 11: March 15=====
+Tuesday: Data refinement and Procedural Refinement. Illustration of these concepts using the Birthday Book example in which we write an initial specification, do a data refinement, followed by a procedural refinement; finally a merge produces code.
+Thursday: Labtest2
+===== Week 12: March 22=====
+Tuesday: Dijkstra weakest precondition calculus and loop variants and invariants.Proving loop termination. Relationship of Dijkstra weakest precondition calculus to Event-B. Slides on the SVN.
+Thursday: Review of arithmetic, set theory, predicate logic and Event-B invariant and refinement proof obligations. Translation between set theoretic statements and predicate logic. Re-write rules.
+===== Week 13: March 29=====
+Work through a complete example: requirements document, initial specification, refinements etc.