Differences

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

--- course_outline [2015/04/07 23:42] – jonathan
+++ course_outline [2015/04/07 23:51] (current) – jonathan
@@ Line 8: / Line 8: @@
   * 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 47: / Line 47: @@
 ===== Hoare Logic  =====
-See slides 10. Hoare logic, program verification and and Dijkstra's urn problem
+See slides 10. Hoare logic, program verification and and Dijkstra's urn problem.
+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 =====
@@ Line 55: / Line 61: @@
   * [[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  =====