Differences

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

--- course_outline [2015/04/07 23:48] – jonathan
+++ course_outline [2018/01/03 02:03] (current) – jonathan
@@ Line 2: / Line 2: @@
 The course outline is a guideline to topics that will be discussed in the course, and when they will be discussed:
+===== Introduction =====
+Use this small project to get started with Event-B and the Rodin tool
+  * {{:01-intro-bank.pdf|Simple Bank System}}. Introduction to Specification and Refinement.
+  * [[https://youtu.be/aROKK2HKhog|Video Presentation]]
 ===== Reactive systems: Bridge =====
@@ Line 8: / Line 17: @@
   * 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 49: / Line 58: @@
 See slides 10. Hoare logic, program verification and and Dijkstra's urn problem.
-C.A.R Hoare won the Turing Award in 1980.
+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 =====
+[[http://lamport.azurewebsites.net/video/videos.html|TLA Videos]]
 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.
@@ Line 66: / Line 80: @@
 ===== 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.
+The following examples are unlikely to be on the exam.
+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.