Differences

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

--- course_outline [2012/03/06 04:26] – jonathan
+++ course_outline [2012/04/03 20:06] (current) – jonathan
@@ Line 52: / Line 52: @@
-**Exercise in preperation for Labtest2**: Do the initial model of the celebrity example (from the Exercises). Formalize the problem in Event-B using a "knows" relation. Recall the indentity and inverse relations and show how the Celebrity axioms could be written in predicate logic or set theory. The celebrity example is one of the exercises that you must do in advance of Labtest2.
+**Exercises 11 and 12 in preparation for Labtest2**: Ex 11: ftp protocol. Ex12: Do the initial model of the celebrity example (from the Exercises). Formalize the problem in Event-B using a "knows" relation. Recall the indentity and inverse relations and show how the Celebrity axioms could be written in predicate logic or set theory. The celebrity example is one of the exercises that you must do in advance of Labtest2.
@@ Line 61: / Line 61: @@
-===== Sequential Prtograms =====
+===== Sequential Programs =====
 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]].
-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.
+Discussion. (a) 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. (b) BAG abstract datatype.
-BAG abstract datatype.
+In class we provided the following requirement:
-===== Week 12=====
+REQ: Find an integer approximation to the square root of n.
+**Specification**
+  n,d: INT
+  sqrt
+    require n >= 0
+    ensure (d^2 <= n < (d+1)^2) & (n = old n)
+Problem: Convert the above specification ito Rodin and use Rodin refinement rules to develop the code for the method //sqrt//.
+We did the celebrity problem ind detail including the addition of a variant for the new event and witnesses for disappearing parameters. We also studied injections, surjection and bijections of functions and relations. See Rodin folder.
+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.
+===== Weakest Preconditions=====
+We did not cover weakest preconditions.
+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.
-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=====
-Work through a complete example: requirements document, initial specification, refinements etc.