정형 명세(formal specification)는 수학의 엄밀한 정의를 이용 하여 요구 사항을 분명하고 간결하게 기술한다. 정형 명세 중에서 집합, 시퀀스(sequence)와 같은 수학적 모델을 이용해서 시스템의 상태 및 상태변화를 추상적으로 기술하는 것을 모델－기반 명세 (model－based specification)라고 한다. 모델－기반 명세와 거리가 먼 것은?