정형 명세(Formal Specification) 훑어보기

V&V 노트에서 “우리가 만든 게 제대로 만들어졌는가”와 “설계도대로 만들었는가”를 구분했는데, 그 “설계도” 자체를 수학적으로 애매함 없이 쓰는 방법이 정형 명세임 자연어 요구사항은 사람마다 다르게 해석할 여지가 있지만, 정형 명세는 그 여지를 없애는 게 목표

자연어 명세의 문제

“시스템은 응답을 빠르게 반환해야 한다” — “빠르게”가 1초인지 100ms인지, 누가 봐도 다르게 읽힐 수 있음 정형 명세는 이런 모호함을 수학적 표기(집합론, 논리식)로 없앰

Z Notation: 집합론과 술어논리 기반으로 시스템 상태와 연산을 명세 상태를 스키마(schema) 단위로 쪼개 “이 연산 전에는 이 조건, 후에는 이 조건”을 명시
B-Method: Z와 비슷한 계열이지만, 명세에서 실제 구현 코드로 단계적으로 정제(refinement)하는 과정 자체가 방법론에 포함됨 프랑스 철도 신호 시스템처럼 사람 생명이 걸린 시스템에서 실제로 쓰인 이력이 있음

버그 없는 소프트웨어를 “테스트로 증명”하는 건 사실상 불가능하다(모든 입력을 다 시도할 수 없으니까) 정형 명세는 반대로 “수학적으로 증명”하는 접근이라, 특히 실패하면 안 되는 시스템(항공, 원자로 제어, 암호 프로토콜)에서 여전히 쓰임

현실적인 한계

정형 명세는 비용이 매우 큼 시스템 전체를 명세하는 게 아니라, 실패 시 피해가 치명적인 핵심 모듈에만 선택적으로 적용하는 게 실무 접근임

원본: V&V