Specifications

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

Contracts and Assertions - slide 4 : 32

Specifications

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

What - not how.

Abstract Datatypes - Specification of

Formal techniques for specification of abstract datatypes
- Algebraic specifications
  - Equations that define how certain operations work on constructor expressions
- Axiomatic specifications
  - Logical expressions - assertions - associated with classes and operations
  - Often divided into invariants, preconditions, and postconditions

An algebraic specification of a stack.

An axiomatic specification of the squareroot function.