명세와 구현의 간극, 버그가 숨는 곳
대부분의 버그는 명세가 묘사하는 것과 코드가 실제로 하는 것 사이의 간극에서 생깁니다. 형식 명세가 그 틈을 어떻게 좁히는지 알아봅니다.
James Whitfield
프로그래밍 언어 이론 커뮤니티에서는 가끔 이런 주장이 나옵니다. ‘충분히 상세한 명세는 코드와 구별할 수 없다.’ 도발적인 주장이죠. 프로그램이 무엇을 해야 하는지 설명하는 것과 실제로 그렇게 동작하게 만드는 것 사이의 선이 생각보다 얇다는 뜻입니다. 명세가 모호함을 완전히 없앨 만큼 정밀하다면, 사실상 프로그램을 이미 작성한 셈입니다.
이건 그저 철학적 논쟁만은 아닙니다. 소프트웨어를 만드는 방식, 명세가 맡는 역할, 그리고 대부분의 버그가 코딩 실수가 아니라 명세의 빈틈에서 나온다는 사실과 직결됩니다. 명세가 어디서 끝나고 구현이 어디서 시작하는지 이해하면, 테스트와 타입, 정확성을 바라보는 시각이 달라집니다.
대부분의 버그는 어디서 오는가
개발자에게 버그가 어디서 오냐고 물으면 보통 ‘코드’라고 답합니다. 하지만 소프트웨어 결함을 연구한 자료들을 보면 다른 결론이 나옵니다. 대부분의 버그는 의도와 구현 사이의 간극에서 생깁니다. 코드는 개발자가 시킨 대로 정확히 동작합니다. 다만 명세가 형식적이든 비형식적이든 모호하거나 불완전하거나 잘못 이해되어서, 개발자가 엉뚱한 것을 시킨 것입니다.
전형적인 예를 하나 들어보죠. 명세에 ‘시스템은 동시 요청을 처리해야 한다’라고 적혀 있다고 합시다. ‘처리한다’는 무슨 뜻일까요? 순서대로 처리하나요, 동시에 처리하나요? 너무 많이 들어오면 큐에 넣나요? ‘너무 많이’는 몇 개인가요? 큐가 가득 찬 상태에서 들어오는 요청은 어떻게 하죠? 이런 질문들은 구현 세부사항이 아니라 명세의 빈틈입니다. 답하지 않은 질문마다 잠재적인 버그가 하나씩 생깁니다. 개발자가 구현을 통해 암묵적으로 답을 내리는데, 그 답이 사용자나 다른 개발자의 기대와 어긋날 수 있기 때문입니다.
명세 정밀도의 스펙트럼
명세는 비형식적인 것에서 형식적인 것까지 스펙트럼을 이룹니다.
- 자연어. ‘로그인 시스템은 안전하고 사용하기 편리해야 한다.’ 이건 명세라기보다 소망에 가깝습니다. 모든 단어가 모호하죠. ‘안전하다’는 무엇을 말할까요? ‘사용하기 편리하다’는 또 무엇일까요? 요구사항처럼 보이지만 실은 판단을 미뤄 둔 문장입니다.
- 구조화된 자연어. ‘사용자가 10분 안에 잘못된 비밀번호를 세 번 입력하면 계정을 30분 동안 잠근다.’ 앞의 것보다 정밀하지만 여전히 모호합니다. ‘잘못된 비밀번호’에 빈 값 제출도 포함되나요? 세 번의 시도가 연속이어야 하나요? 10분 창은 슬라이딩인가요, 고정인가요?
- 타입 시그니처.
authenticate(username: string, password: string) -> Result<User, AuthError>. 함수의 인터페이스는 정확히 명시하지만 동작에 대해서는 아무 말도 하지 않습니다. 입력과 출력의 모양은 알지만, 둘 사이의 관계는 모릅니다. - 속성 기반 명세. ‘데이터베이스에 있는 모든 유효한 사용자명-비밀번호 쌍에 대해,
authenticate는user.username == username인Ok(user)를 반환한다.’ 논리 한정자를 써서 동작을 더 정밀하게 제약합니다. - 형식 명세. 시스템 동작의 완전한 수학적 모델로, 모든 상태, 모든 전이, 모든 불변식을 담습니다. 이 수준에 이르면 명세와 구현은 거의 같은 것이 됩니다.
형식 명세에 가까워질수록 모호함의 여지는 줄고, 버그가 숨을 자리도 줄어듭니다. 하지만 한 단계씩 올라갈 때마다 드는 노력과 필요한 전문 기술도 커집니다. 실무에서 던질 질문은 이것입니다. 주어진 프로젝트에서 이 스펙트럼을 어디까지 올라가야 할까?
가벼운 명세로서의 타입
타입 시스템은 일상 프로그래밍에서 가장 널리 쓰이는 명세 형태입니다. 동작을 묘사하지는 않지만 동작을 제약합니다. User 대신 Option<User>를 반환하는 함수는 사용자를 찾지 못할 수도 있다고 명시하고, 컴파일러는 호출하는 모든 쪽이 그 가능성을 처리하도록 강제합니다.
// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User // What if ID is invalid?
// // What if user not found?
// // Does it panic? Return null?
// // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.Rust, Haskell, TypeScript 같은 언어들은 형식 기법 훈련 없이도 표현력 높은 타입 시스템이 명세의 간극을 얼마나 줄일 수 있는지 보여 줍니다. 대수적 데이터 타입, 제네릭 제약, 빠짐없는 패턴 매칭이 함께 타입 수준에서 프로그램 동작의 많은 부분을 명시하고, 컴파일러가 이를 자동으로 검증합니다.
핵심은 이겁니다. 모든 타입 어노테이션은 자동으로 검사되는 명세입니다. 타입 시스템으로 인코딩할 수 있는 동작 하나하나는, 여러분이 절대 겪지 않을 버그 부류 하나입니다.
속성 기반 테스트: 동작을 명세하기
단위 테스트는 예시 기반 명세입니다. ‘이 특정 입력에는 이 특정 출력이 나와야 한다.’ 유용하지만 본질적으로 불완전합니다. 떠올린 경우만 테스트할 수 있으니까요. 속성 기반 테스트는 이를 뒤집습니다. 모든 입력에 대해 성립해야 하는 속성을 명세하고, 테스팅 프레임워크가 무작위 입력을 생성해 위반 사례를 찾아냅니다.
from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.이 테스트의 세 가지 속성은 단순히 정렬을 테스트하는 데 그치지 않고, 정렬이 무엇인지를 정의합니다. 세 속성을 모두 만족하는 함수는 정의상 올바른 정렬입니다. 이것이 ‘코드로서의 명세’라는 아이디어를 가장 실용적으로 보여 주는 형태입니다. 올바른 동작을 정의하는 속성을 작성하고, 구현이 그 속성을 만족하는지 테스팅 프레임워크가 검증하게 하면 됩니다.
TLA+와 모델 체킹
버그 하나의 비용이 막대한 시스템, 예컨대 분산 시스템, 금융 플랫폼, 핵심 인프라에서는 TLA+ 같은 형식 명세 도구가 더 강한 보장을 제공합니다. TLA+(Temporal Logic of Actions)는 시스템 동작을 상태 기계로 명세하고 모델 체킹을 할 수 있게 해 줍니다. 가능한 모든 실행 경로를 빠짐없이 탐색해서 불변식이 성립하는지 확인하는 것입니다.
Amazon은 S3, DynamoDB 등 핵심 AWS 서비스의 알고리즘을 검증하는 데 TLA+를 써 왔습니다. 테스트로는 거의 찾을 수 없었을 버그들을 찾아냈다고 공개적으로 설명했는데, 수백만 번 실행 중 한 번 나올까 말까 한 동시 연산의 특정 인터리빙에서만 드러나는 버그였습니다.
Raft 같은 합의 프로토콜의 TLA+ 명세는 보통 수백 줄 정도입니다. 합법적인 상태 전이를 모두, 모든 불변식(예: ‘한 임기에 리더는 최대 한 명’), 그리고 모든 안전성 속성을 기술합니다. 모델 체커는 수십억 개의 가능한 실행 경로를 탐색하며 어떤 경로도 불변식을 깨지 않는지 확인합니다. 기계적으로 구현으로 번역할 수 있을 만큼 정밀한, 실제로 코드에 가까운 명세입니다.
계약에 의한 설계
Bertrand Meyer의 계약에 의한 설계(DbC)는 실용적인 중간 지점에 자리합니다. 각 함수는 사전 조건(함수 호출 전에 참이어야 하는 것), 사후 조건(반환 시 함수가 보장하는 것), 불변식(객체에 대해 항상 참이어야 하는 것)을 명시합니다. 이 계약은 개발 중 런타임에 검사되고, 성능을 위해 프로덕션에서는 선택적으로 끌 수 있습니다.
def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount송금 전후의 총액이 같아야 한다는 보존 사후 조건은, 단위 테스트가 거의 다루지 않는 버그를 잡아내는 종류의 불변식입니다. 돈은 생성되거나 소멸되지 않는다는 시스템의 근본 속성을 명시하며, 올바른 구현이라면 반드시 만족해야 합니다.
실용적인 권장 사항
대부분의 소프트웨어에 완전한 형식 명세는 현실적이지 않습니다. 하지만 일반적인 개발 워크플로에 들어가는 기법만으로도 명세의 간극을 상당히 줄일 수 있습니다.
- 타입 시스템을 적극 활용하세요. 가능하면 제약을 타입으로 인코딩하세요. 리스트가 비어 있으면 안 될 때는
List대신NonEmptyList를 쓰세요. 둘 다 문자열이더라도 newtype 래퍼로UserId와OrderId를 구별하세요. 타입으로 인코딩한 제약은 컴파일러가 공짜로 검사해 주는 제약입니다. - 핵심 로직에는 속성 기반 테스트를 작성하세요. 시스템이 유지해야 할 불변식을 찾아 속성 테스트로 표현하세요. 잘 고른 속성 몇 개만으로도 수천 개의 예시 기반 테스트가 놓치는 버그를 잡아냅니다.
- 경계를 명세하세요. 가장 중요한 명세는 시스템 경계에 있습니다. API 계약, 데이터베이스 스키마, 메시지 포맷이 그렇습니다. OpenAPI 명세, Protocol Buffers, JSON Schema를 써서 기계가 검증할 수 있게 만드세요.
- 핵심 동시성 시스템에는 TLA+나 Alloy를 쓰세요. 합의 알고리즘, 분산 락, 금융 트랜잭션 시스템을 설계한다면, 형식 명세에 드는 비용은 프로덕션에서 미묘한 정확성 버그가 터졌을 때의 비용에 비하면 작습니다.
- 테스트보다 명세를 먼저 쓰세요. 올바른 동작이 어떤 모습인지 정확히 말할 수 없다면, 그것을 검증할 수도 없습니다. 함수가 무엇을 해야 하는지 모든 경우(엣지 케이스 포함)를 명확히 적는 데 30분을 투자하면, 코드를 한 줄 쓰기 전에 설계 문제가 드러나는 경우가 많습니다.
‘충분히 상세한 명세는 코드다’라는 주장은 정확히 맞지는 않습니다. 더 정확히 말하면, 충분히 상세한 명세는 버그가 자리할 여지를 없앱니다. 명세와 구현 사이의 간극에 모호함이 살고, 버그는 그 모호함에서 자랍니다. 타입, 속성, 계약, 형식 기법 등 그 간극을 좁히는 기법은 모두 소프트웨어를 더 올바르게 만듭니다. 코딩 실수를 막아 주기 때문이 아니라, 코딩 실수의 뿌리인 명세 실수를 막아 주기 때문입니다.
