Differences

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

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