Differences

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

--- course_outline [2012/03/06 04:29] – jonathan
+++ course_outline [2012/04/03 20:06] (current) – jonathan
@@ Line 67: / Line 67: @@
 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.
+In class we provided the following requirement:
+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=====
-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.
+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.
-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.