Software correctness is becoming an increasingly important concern as our society grows more and more reliant on computer systems. Even the simplest of software errors can have devastating financial or security consequences. How can we find errors in real-world applications?  How can we guarantee that such errors don't exist?  To even begin to answer these questions we need a specification: a description of what it means for a piece of code to be correct, stated either explicitly (e.g. my private data are never leaked to third parties) or implicitly (e.g. this code will not terminate with an uncaught exception).