Advances in Programming Languages 2018/19 Lecture 12: Specification and Verification

Today's lecture was the first in a block on language techniques and tools that aim to improve program correctness: not necessarily changing what a program does, the time or space it takes, or the power it uses; but making sure that what it does is the right thing to do. Of course, that also requires having some way to identify what that is to begin with.

This lecture looked in particular at Hoare Logic a language for specifying desired behaviour, and a little about ways to confirm that a program meets a specification.

Media Hopper Create does not permit public attachments to videos, so for the corresponding slides you will need to use this alternate server: https://wp.inf.ed.ac.uk/apl18/wp-content/uploads/sites/10/2018/10/apl18-12.pdf