introduces: sort1, sort2, ... , sortN .
needs: spec1, spec2, ... , specN.
op opName :: arg1 , ... , argN -> result .
Sort relation formulae: define the relationships for the specification-defined sorts. There are two kinds of possible formulae: the sort equality (eq sort1 = sort2) and the subsort equation (eq sort1 <= sort2).