형식 명세: 명령어를 넘어 소프트웨어 동작 정의하기
2025-07-28
이 글에서는 형식 명세와 기존 프로그램의 차이점을 자세히 살펴봅니다. 프로그램은 명령어 목록이지만, 형식 명세는 동작의 집합입니다. 저자는 카운터 예시를 사용하여 명세가 모든 올바른 동작을 어떻게 정의하고, 집합 이론을 활용하여 생성기(Init 및 Next)를 통해 무한한 동작 집합을 어떻게 설명하는지 보여줍니다. 이는 프로그래밍에서의 비결정성 개념과 대조됩니다. 형식 명세에서의 비결정성은 동작을 확장할 수 있는 여러 가지 방법을 의미하지만, 프로그램에서의 비결정성은 불확실한 코드 경로를 의미합니다. 이 글에서는 디버깅 및 모델 검사기 오류 해석에 필수적인 동작 집합으로서 형식 명세를 이해하는 중요성을 강조합니다.