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.
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336, VAT Registration Number GB 592 9507 00, and is acknowledged by the UK authorities as a “Recognised body” which has been granted degree awarding powers.