175. 요구사항 명세 언어 (Z, VDM 등 정형 언어)

핵심 인사이트 (3줄 요약)

본질: 요구사항 명세 언어는 시스템이 "무엇을 만족해야 하는가"를 표현하는 약속이며, 자연어 중심의 비정형 명세부터 수학 기반 정형 명세까지 정밀도 스펙트럼을 가진다.

가치: Z Notation, VDM (Vienna Development Method) 같은 정형 언어는 상태, 불변식, 사전조건, 사후조건을 엄밀하게 적어 요구사항의 모순과 누락을 코드 작성 전에 검토하게 해 준다.

판단 포인트: 사용자 화면처럼 변화가 잦은 영역은 비정형·반정형이 효율적이지만, 안전·금융·보안·프로토콜 핵심 규칙처럼 실패 비용이 큰 영역은 정형 명세를 선택할수록 해석 오차를 줄일 수 있다.

Ⅰ. 개요 및 필요성

요구사항 명세 언어는 이해관계자가 같은 요구를 같은 뜻으로 읽게 만드는 표현 도구다. 문제는 자연어가 매우 편한 대신 매우 모호하다는 점이다. "빠르게 응답해야 한다", "5번 실패하면 계정을 잠근다", "적절한 권한만 허용한다" 같은 문장은 회의에서는 통하지만, 설계와 구현 단계에서는 서로 다른 해석을 낳기 쉽다.

이 개념이 중요한 이유는 소프트웨어 오류가 코드 이전에 이미 요구사항 문장 속에서 시작되기 때문이다. 분석가는 누적 5회를 생각하고, 개발자는 연속 5회를 구현하고, 시험자는 세션 단위 초기화를 기대하면 같은 문서를 읽고도 서로 다른 시스템을 만든다. 명세 언어는 이 해석의 틈을 줄이는 장치이며, 정형성 수준이 높아질수록 틈은 줄지만 작성 비용과 학습 비용은 커진다.

아래 그림은 모호한 요구가 어떻게 단계별로 다른 시스템으로 분기되는지를 보여 준다.

┌────────────────────────────────────────────────────────────────────┐
│ Ambiguity propagation                                              │
├────────────────────────────────────────────────────────────────────┤
│ requirement: "lock account after 5 failures"                      │
│        │                     │                     │               │
│        ▼                     ▼                     ▼               │
│  analyst view          developer view         tester view          │
│  cumulative 5          consecutive 5          reset by session     │
│        └─────────────────────┬─────────────────────┘               │
│                              ▼                                     │
│                 different design, code, and test oracles           │
└────────────────────────────────────────────────────────────────────┘

따라서 요구사항 명세 언어는 단순한 문서 스타일이 아니라, 오해 비용을 어디까지 줄일 것인가에 대한 관리 전략이다. 시스템 위험이 커질수록 "편하게 쓴 문장"보다 "검증 가능한 표현"이 더 중요해진다.

📢 섹션 요약 비유: 요구사항 명세 언어는 같은 여행 계획을 말로 대충 정할지, 좌표와 시간표까지 적은 여행표로 맞출지 정하는 약속과 같다.

Ⅱ. 아키텍처 및 핵심 원리

요구사항 명세 언어는 보통 비정형 (Informal), 반정형 (Semi-formal), 정형 (Formal) 세 층으로 이해하면 쉽다. 비정형은 자연어, user story, 서술형 문장을 주로 쓰며 이해관계자 소통에 강하다. 반정형은 Unified Modeling Language (UML), 상태도, decision table처럼 구조와 표기 규칙을 일부 가진다. 정형은 수학적 논리와 집합, 상태 전이 모델을 사용해 모호함을 최소화한다.

구분	표현 수단	장점	약점	대표 예
비정형	자연어, 회의록, user story	이해하기 쉽고 빠름	모호성, 누락, 해석 차이	Software Requirements Specification (SRS) 서술형 문장
반정형	UML, 상태도, decision table	구조 공유와 시각화에 강함	일부 의미는 여전히 자연어 의존	use case, activity/state diagram
정형	수학 기호, 논리, 타입, 불변식	검증 가능, 모호성 최소	학습 비용과 작성 비용 큼	Z Notation, VDM, B-Method

정형 명세의 핵심 구성요소는 크게 네 가지다. 첫째, 상태 (State): 시스템이 보유한 변수와 데이터 구조. 둘째, 불변식 (Invariant): 어떤 순간에도 깨지면 안 되는 제약. 셋째, 사전조건 (Precondition): 연산이 실행되기 위해 만족되어야 할 조건. 넷째, 사후조건 (Postcondition): 연산 후 반드시 성립해야 할 결과다. Z는 이를 schema 중심으로 조직하고, VDM은 보다 프로그램에 가까운 표현으로 데이터 타입과 연산을 기술한다.

예를 들어 계좌 시스템에서 balance는 0 이상이어야 하고, Withdraw(amount)는 amount <= balance일 때만 실행되며, 실행 후에는 balance' = balance - amount가 되어야 한다. 이 한 줄이 중요한 이유는 구현 전에 이미 "잔액 음수 허용 여부", "출금 가능 조건", "상태 변화 결과"가 명확해지기 때문이다.

아래 그림은 정형 명세가 요구를 어떤 구조로 묶는지 보여 준다.

┌────────────────────────────────────────────────────────────────────┐
│ Structure of a formal specification                                │
├────────────────────────────────────────────────────────────────────┤
│ state variables -> invariant -> allowed operations                 │
│                                   │                                │
│                                   ├─ precondition                  │
│                                   ├─ state transition              │
│                                   └─ postcondition                 │
│ result: analyzable model before code exists                        │
└────────────────────────────────────────────────────────────────────┘

즉 정형 언어의 힘은 "예쁘게 적는다"가 아니라, 명세를 분석 가능한 모델로 바꾸는 데 있다. 이 모델은 theorem proving, model checking, test case derivation 같은 후속 검증 활동과도 자연스럽게 연결된다.

📢 섹션 요약 비유: 비정형 명세가 말로 설명한 요리법이라면, 정형 명세는 재료·온도·시간·금지 조건까지 적힌 실험실 프로토콜에 가깝다.

Ⅲ. 비교 및 연결

명세 언어를 비교할 때 핵심은 "누가 읽기 쉬운가"보다 "어디까지 같은 뜻으로 읽히는가"다. 비정형 명세는 빠른 합의와 범위 탐색에 좋지만, 해석 차이를 자동으로 막지 못한다. 반정형 명세는 흐름과 상태를 드러내는 데 강해 아키텍처 커뮤니케이션에 유리하다. 정형 명세는 가장 비싸지만, 가장 엄밀하게 요구를 고정한다.

관점	비정형 명세	반정형 명세	정형 명세
가독성	높음	중간	낮을 수 있음
모호성 통제	낮음	중간	높음
자동 분석 가능성	거의 없음	일부 있음	높음
변경 대응 속도	빠름	보통	느릴 수 있음
적합 영역	초기 탐색, 사용자 소통	구조 설계, 인터페이스 공유	고위험 규칙, 핵심 제약

이 차이는 개발 생명주기와도 연결된다. 비정형 명세는 stakeholder interview와 scope negotiation에 강하고, 반정형 명세는 아키텍처 리뷰와 팀 간 합의에 강하다. 정형 명세는 구현 전 논리 검토, 안전성 증명, test oracle 생성에 강하다. 따라서 셋은 대체재라기보다, 프로젝트 위험과 목적에 따라 조합해야 하는 표현 계층이다.

또한 정형 명세는 Design by Contract, state machine testing, formal verification과도 자연스럽게 이어진다. 사전조건·사후조건은 코드 수준 계약으로 내려갈 수 있고, 상태 전이 모델은 test case의 기반이 된다. 즉 좋은 명세 언어는 문서에서 끝나는 것이 아니라, 설계·검증·테스트로 연쇄적으로 이어진다.

📢 섹션 요약 비유: 비정형·반정형·정형 명세는 각각 메모, 설계도, 법률 문서처럼 정밀도가 다른 표현 체계라서 목적에 맞게 섞어 써야 한다.

Ⅳ. 실무 적용 및 기술사 판단

실무에서 중요한 질문은 "정형 명세가 좋은가?"가 아니라 "어디까지 정형화할 가치가 있는가?"다. 사용자 인터페이스 문구, 마케팅 화면, 빠르게 바뀌는 기능 가설은 비정형이나 반정형으로도 충분히 관리할 수 있다. 반면 계좌 잔액 일관성, 접근 제어 규칙, 의료기기 안전 제약, 프로토콜 상태 전이는 해석 오차 비용이 매우 크므로 정형 명세의 투자 가치가 커진다.

아래 판단 흐름은 어떤 수준의 명세 언어를 택할지 결정할 때 사용할 수 있다.

┌────────────────────────────────────────────────────────────────────┐
│ Choosing the specification language                                │
├────────────────────────────────────────────────────────────────────┤
│ failure cost high or regulation strict?                            │
│   ├─ yes -> formal core model (Z / VDM / proof-oriented review)    │
│   └─ no                                                            │
│        ├─ many teams need shared structure? -> semi-formal model   │
│        └─ rapid discovery and change? -> informal text + examples  │
└────────────────────────────────────────────────────────────────────┘

실무 판단 기준

실패 비용: 장애가 금전 손실, 법적 문제, 안전 사고로 직결되는가?
규칙 안정성: 자주 바뀌는 화면 요구인지, 오래 유지될 핵심 도메인 규칙인지?
동시성·상태 복잡도: 상태 전이와 예외 조건이 많아 자연어로 관리하기 어려운가?
조직 역량: 팀이 Z, VDM, model checker 같은 도구와 표기를 소화할 수 있는가?
산출물 연결성: 명세가 실제 test case, contract, code review 기준으로 이어질 수 있는가?

자주 나오는 안티패턴

안전·금융 핵심 규칙을 자연어 한 문장으로만 남겨 해석 차이를 방치하는 것
반대로 자주 바뀌는 화면 시안을 처음부터 전면 정형화해 과도한 비용을 쓰는 것
정형 모델을 한 번 만든 뒤 코드와 동기화하지 않아 "정확하지만 오래된 문서"로 만드는 것

실무에서 가장 현실적인 방법은 계층적 사용이다. 예를 들어 제품 요구는 자연어와 예제로 공유하고, 화면 흐름은 UML 상태도나 decision table로 구조화하며, 금전 정산·권한 검증·안전 인터록 같은 핵심 규칙만 Z나 VDM 수준으로 엄밀하게 고정하는 식이다. 이렇게 해야 설명력과 정확성을 동시에 얻을 수 있다.

📢 섹션 요약 비유: 명세 언어 선택은 모든 방을 방탄문으로 만들지, 현관과 금고만 방탄 처리할지 결정하는 보안 설계와 같다.

Ⅴ. 기대효과 및 결론

명세 언어를 적절히 선택하면 요구사항 오해가 줄고, 설계와 테스트의 기준점이 선명해진다. 정형 수준이 높아질수록 모순과 누락을 더 이른 단계에서 발견할 수 있고, 규제가 강한 산업에서는 감사 가능성과 설명 책임도 좋아진다. 특히 핵심 불변식이 명세에 박혀 있으면 구현 변경이 일어나도 무엇을 절대 깨면 안 되는지 팀 전체가 공유할 수 있다.

물론 정형 명세가 만능은 아니다. 도메인 지식이 부족하면 수학적으로 적어도 틀린 모델이 될 수 있고, 모델 유지보수에 실패하면 코드와 문서가 다시 벌어진다. 또한 모든 요구를 정형화하는 것은 비용이 크므로, 위험 기반 선택이 항상 전제되어야 한다.

정리하면 요구사항 명세 언어는 문서 취향의 문제가 아니라, 프로젝트의 위험과 커뮤니케이션 비용을 조절하는 제어 레버다. 기억할 핵심은 분명하다. 비정형은 빠른 이해를, 반정형은 구조적 공유를, 정형은 해석 오차 최소화를 담당하며, 좋은 엔지니어링은 이 세 층을 적절히 배치하는 데서 나온다.

📢 섹션 요약 비유: 명세 언어는 같은 건물을 짓더라도 스케치, 설계도, 구조 계산서를 어디까지 준비할지 정하는 과정과 같아서, 건물이 중요할수록 문서도 더 정밀해져야 한다.

📌 관련 개념 맵

개념	연결 포인트
모호성 (Ambiguity)	명세 언어가 줄이려는 가장 직접적인 문제다.
불변식 (Invariant)	시스템이 어떤 상태에서도 지켜야 할 핵심 규칙을 정의한다.
사전조건 / 사후조건 (Precondition / Postcondition)	연산의 허용 범위와 결과 보장을 명시한다.
Unified Modeling Language (UML)	반정형 명세의 대표 도구로 구조와 흐름을 공유한다.
형식 검증 (Formal Verification)	정형 명세를 바탕으로 구현과 요구의 일치 여부를 분석한다.
Design by Contract	명세의 조건 개념을 코드 수준 계약으로 연결하는 방법이다.

📈 관련 키워드 및 발전 흐름도

stakeholder need
    │
    ▼
informal text and examples
    │
    ▼
semi-formal models (UML / decision table)
    │
    ▼
formal state + invariant + operation model
    │
    ▼
verification / test derivation / auditability

이 흐름도는 요구사항 표현이 단순 문장에서 시작해 구조화된 모델과 정형 검증으로 발전할 수 있으며, 프로젝트 위험이 커질수록 더 정밀한 계층으로 이동한다는 점을 보여 준다.

👶 어린이를 위한 3줄 비유 설명

하고 싶은 일을 말로만 설명하면 듣는 사람마다 조금씩 다르게 알아들을 수 있어요.
그림과 규칙표를 쓰면 더 비슷하게 이해하고, 수학처럼 아주 정확히 쓰면 거의 틀리지 않게 약속할 수 있어요.
그래서 중요한 기계일수록 설명도 더 정확한 언어로 써야 해요.