Lecture overview -- Keyboard shortcut: 'u'  Previous page: Correctness -- Keyboard shortcut: 'p'  Next page: Specification with preconditions and postconditions [Section] -- Keyboard shortcut: 'n'  Lecture notes - all slides together  Annotated slide -- Keyboard shortcut: 't'  Textbook -- Keyboard shortcut: 'v'  Alphabetic index  Help page about these notes  Course home    Contracts and Assertions - slide 4 : 32


A program specification is a definition of what a computer program is expected to do [Wikipedia].

What - not how.

An algebraic specification of a stack.
An axiomatic specification of the squareroot function.