Under construction. See ExtremeCatalysis

I am just listing the points now, I'll flesh them later.
Also examples coming up.

In specs, you can use (1) invariants (2) convenience attributes
(3) abstraction and retrieval functions.

In code, invariants must be very limited, because they have
to be easy to compute. In specs, invariants can be used to
abstract certain kinds of computation.

''Why not put the invariant in the unit test?  Then there isnt a performance issue in the release code - TimWoodard''

In programs, implementation restrictions limit the amount
of "data" you can have. Specs have no such limitation.  ''Specs have the limitation that they have to be usable by humans; that limits the amount of information you can stuff into them.  If you can't hold an abstraction of the system in your head, you can't implement it.  If you can't write the abstraction concisely, it won't fit in your head.''