University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Lecture 3: Logic for Program Development

Lecture 3: Logic for Program Development

Add to your list(s) Download to your calendar using vCal

  • UserTony Hoare, FRS FREng
  • ClockFriday 04 May 2018, 14:00-15:00
  • HouseFW26.

If you have a question about this talk, please contact Victor Gomes.

Tony Hoare, FRS FR Eng, Hon Mem Cambridge University Computing Laboratory.

Logic is used for reasoning at all stages of program description and development. We extend the standard notations for program specification (assertions and assumptions) by notations for description of the actions, objects, events, causality and synchrony that feature in each individual trace of execution. The description of the behaviour of a program defines the whole set of its possible traces, both correct and erroneous. Each operator on traces is defined (lifted) as a function of the descriptions of its operands. Logical disjunction of descriptions introduces the element of choice into the programming language; the lifted operators distribute through choice, and the other algebraic laws of program development are preserved. Standard predicate calculus, enriched by programming operators may now be used for reasoning about program specification, design, documentation, evolution, and testing.

Attendance at the previous lecture is not a prerequisite.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2018, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity