Differences

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

--- course_outline [2010/03/02 04:22] – jonathan
+++ course_outline [2010/03/25 20:56] (current) – jonathan
@@ Line 82: / Line 82: @@
 **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.