"Documentation by paper"

[Robert Dewar]

> I would add that a real spec tells you what the function _does_ and
> sometimes how to use it, in addition to pre/postconditions :)

It also might have *some* details of the implementation if they are
important to its use, e.g. knowing whether a sort is nlogn or n**2.

Of course sufficiently powerful pre and post conditions would be able
to describe what a function does, but if these conditions are written
in a low level language without set comprehension and quantifiers, this
can be impractical in practice.