I also think universal quantifiers ("for all ...") are a key distinguishing feature of specs. For example, a spec for a shortest path algorithm can be much simpler than any actual algorithm, largely because we can quantify over all (potentially infinitely many) paths:

FORALL paths P from A to B:

  |shortestPath(A,B)| <= |P|