Differences

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

--- course_outline [2012/03/13 17:01] – jonathan
+++ course_outline [2012/04/03 20:06] (current) – jonathan
@@ Line 74: / Line 74: @@
 **Specification**
-n,d: INT
+  n,d: INT
-sqrt
+  sqrt
-  require n >= 0
+    require n >= 0
-  ensure (d^2 <= n < (d+1)^2) & (n = old n)
+    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.