Differences

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

--- course_outline [2014/12/19 19:41] – jonathan
+++ course_outline [2015/04/07 23:51] (current) – jonathan
@@ Line 3: / Line 3: @@
 The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed:
-===== Reactive systems via the bridge example =====
+===== Reactive systems: Bridge =====
  * Read the Rodin Users handbook up to and including Section 2.5.2.
   * Bridge controller (reactive systems) [[http://deploy-eprints.ecs.soton.ac.uk/112/1/sld.ch2.car.pdf|Chapter 2: Controlling cars on a bridge]]).
-    *Required readings: Read Chapters 1 and 2 from the suggested text [[http://www.event-b.org/A_ch2.pdf|chapter 2]]
+  *Required readings: Read Chapters 1 and 2 from the suggested text [[http://www.event-b.org/A_ch2.pdf|chapter 2]]
 Topics covered by the bridge controller include
@@ Line 44: / Line 44: @@
 We study two examples of the development of programs using loops by Dijkstra using the Hoare notation and the proof obligations for loop invariants and variants. Separation of concerns via partial correctness and termination arguments. Weakest preconditions and the wp-axiom for assignment. See also the slides "LoopsAndDisjkstra". This topic is dicussed in detail in Science of Programming (David Gries, chapter 11).
-===== Using Relations =====
-We develop a phone book example by developing a mathematical model from informal E/R-descriptions. We discuss the importance and significance of the relation (and function) override operator. See slides "UsingRelations" in the SVN which includes: relations, relational image, relational inverse, domain and range restrictions and subtractions, and relational composition.
+===== Hoare Logic  =====
-===== More systems =====
+See slides 10. Hoare logic, program verification and and Dijkstra's urn problem.
-We study an EHealth medication system.
+C.A.R Hoare won the Turing Award in 1980. "Hoare made two bold additional steps, and his “An axiomatic basis for computer programming” is one of the most influential papers on the theory of programming. First he discarded the flowcharts and developed a logical system for reasoning about programs using specifications of statement behavior that have become known as Hoare triples. Secondly, he argued that his “axiomatic" system could be viewed as an abstract way of recording the semantics of programming languages.
+The first of these steps has the profound effect of opening up a way of developing provable programs rather than treating their verification as a post hoc concern. Hoare published a number of developments of this idea, and the pursuit of “Hoare semantics" has had a profound effect on the understanding of programming languages and the task of reasoning about programs. There is a fascinating link back to work by Alan Turing in the late 1940s.
+  * [[http://amturing.acm.org/award_winners/hoare_4622167.cfm|Turing Award 1980]]
+  * {{:wiki:hoare-turing-1980.pdf|Award Speech about Hoare Logic}}
+===== TLA+ Thinking for Programmers =====
+See slides 11: Thinking for Programmers. Leslie Lamport's TLA+ specification tool, its use at Amazon and for MS/Xbox 360. Thinking for programmers. QuickSort at the algorithmic level as a divide and conquer algorithm rather than a program. The algorithm can be refined to a recursive implementation, an iterative implementation and a concurrent implementation.
+  * [[http://channel9.msdn.com/Events/Build/2014/3-642|Lamport's Talk]]
+  * [[https://bertrandmeyer.com/2014/12/07/lampsort/|Lampsort as an algorithm in Eiffel]]
+  * Leslie Lamport won the 2013 Turing award for: For fundamental contributions to the theory and practice of distributed and concurrent systems, notably the invention of concepts such as causality and logical clocks, safety and liveness, replicated state machines, and sequential consistency. [[http://amturing.acm.org/award_winners/lamport_1205376.cfm|here]].
+===== Reactive Systems: Train control  =====
+See slides 12. Method for systematic development correct-by-construction reactive systems.
+===== Exam Preparation =====
+Develop a phone book example by developing a mathematical model from informal E/R-descriptions. Relations, Functions and the override operator, relational image, relational inverse, domain and range restrictions and subtractions, and relational composition. See slides 13.
+Develop an Event-B project for an EHealth medication system.
 For the EHealth system the requirements were: