A specification is a way to describe computer-solveable problems and test them, before making the real program.
A specification consists of four parts:
|       |             |
|       | export      |
|common |-------------|
|param- |             |
|eters  | body        |
|       |             |
|       | import      |

export: all the own things you want other specifications to use
body: here is the work done
import: things from other specifications you need
common parameters: The things you im- AND export (ex. imported types which are used in the export)
Please note:
Import!=import (Import=import AND common parameters)
Export!=export (Export=export AND common parameters)
The body consists of the type construction with its operationspecifcations (these are equations which implement your algorithm).