Differences

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

--- course_outline [2012/03/13 17:03] – jonathan
+++ course_outline [2012/04/03 20:06] (current) – jonathan
@@ Line 80: / Line 80: @@
     ensure (d^2 <= n < (d+1)^2) & (n = old n)
-Problem: Convert the following specification ito Rodin and use Rodin refinement rules to develop the code for the method //sqrt//.
+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.