User Tools

Site Tools


course_outline

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
course_outline [2015/04/07 23:48] jonathancourse_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]]).   * 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 Topics covered by the bridge controller include
Line 49: Line 49:
 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. +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}}   * {{:wiki:hoare-turing-1980.pdf|Award Speech about Hoare Logic}}
  
course_outline.1428450538.txt.gz · Last modified: 2015/04/07 23:48 by jonathan

Donate Powered by PHP Valid HTML5 Valid CSS Driven by DokuWiki