대부분의 버그는 “해야 할 일”과 “실제로 하는 일” 사이 틈에 숨어 있다
먼저 코드를 쓰고, 다음에 테스트를 쓰고, 그제야 코드가 틀렸다는 걸 알게 된다. 이게 표준 루프다. 그래서 디버깅은 대부분의 프로젝트 타임라인 절반을 잡아먹는다.
Box Structure는 이를 뒤집는다. 코드를 쓰기 전에 동작을 정의하고, 그 정의를 수학적으로 검증한 뒤, 한 겹씩 코드로 옮긴다. 그 결과는 테스트가 우연히 통과해서 맞는 게 아니라, 구조적으로 올바른 모듈이 된다.
각 겹이 얼마나 작은지 보면 이게 불가능해 보이지 않는다.
Box Structure란 무엇인가
Box Structure는 소프트웨어 모듈을 세 단계의 추상화 수준으로 기술한다. 각 단계는 이전 단계의 엄격한 정제(refinement)다.
- Black Box: 어떤 Stimulus가 어떤 Response를 만드는가? State도 없고, 구현도 없다. 단순히 History에서 Output으로의 Pure Function일 뿐이다.
- State Box: 모듈이 어떤 State를 기억하고, 각 Stimulus가 그 State를 어떻게 변환하여 Response를 만들어내는가?
- Clear Box: 실제 코드.
바깥에서 안으로 설계한다. Black Box는 Contract다. State Box는 Data Model이다. Clear Box는 코드다. 각 단계에서 하위 겹이 상위 겹을 만족하는지 증명한 뒤 다음으로 넘어간다.
이것은 사후 문서가 아니다. Black Box와 State Box는 Formal Specification이다. 그것들이 곧 Design이다. 코드는 가장 나중에 온다.
Black Box: History가 모든 것을 결정한다
Black Box는 모듈을 Stimulus의 History와 Response로 정의한다. 어떤 Stimulus에 대한 Response는 그 이전의 모든 Stimulus에 의존한다.
간단한 Token Bucket Rate Limiter를 생각해 보자. Black Box Specification은 다음과 같다.
| Stimulus | Condition on History | Response |
|---|---|---|
request(n) | tokens available >= n | grant(n) |
request(n) | tokens available < n | deny |
add_tokens(k) | any history | no response, update history |
Black Box는 Token이 어떻게 추적되는지 말하지 않는다. 주어진 Stimulus History에 대해 필요한 Response가 이것이다, 라고 말할 뿐이다.
이것은 코드가 존재하기 전에 검증할 수 있다. Stimulus 시퀀스를 쓰고, 기대 Response를 손으로 계산한 뒤, Specification이 올바르게 동작하는지 확인한다. Compiler도, Test Runner도 필요 없다. 논리만으로 충분하다.
State Box: 가정을 늘리지 않고 기억을 추가한다
State Box는 History를 암묵적으로 만드는 State 변수를 도입함으로써 Black Box를 정제한다. 완전한 Stimulus History를 끌고 다니는 대신, 모듈은 압축된 표현을 기억한다.
Rate Limiter의 경우, State Box는 현재 사용 가능한 Token 수인 tokens을 도입한다. Specification은 다음과 같이 된다.
| Stimulus | Precondition on State | Response | New State |
|---|---|---|---|
request(n) | tokens >= n | grant(n) | tokens - n |
request(n) | tokens < n | deny | tokens (unchanged) |
add_tokens(k) | any | no response | tokens + k |
핵심 단계는 이 State Box가 Black Box와 동등함을 증명하는 것이다. State 변수 tokens은 관련 History를 정확히 표현해야 한다. Black Box의 규칙을 적용한 결과가 State Box Counter와 같은 Response를 내놓으면, 그 정제는 유효하다.
이 증명은 보통 짧다. 검증 대상은 한 페이지짜리 Specification이지, 수천 줄짜리 Codebase가 아니다.
Clear Box: 놀라게 하지 않는 코드
Clear Box는 구현이다. Goto나 숨겨진 Control Flow가 없는 구조화된 언어로 쓰인다. 모든 Clear Box는 Sequence, Alternation(if-then-else), Iteration(while, for)으로 구성된다.
다음은 Python으로 작성한 Clear Box Implementation 예시다.
class TokenBucket:
def __init__(self, capacity: int, refill_rate: float):
self.capacity = capacity
self.tokens = capacity
self.refill_rate = refill_rate
self.last_refill = time.monotonic()
def _refill(self) -> None:
now = time.monotonic()
elapsed = now - self.last_refill
added = int(elapsed * self.refill_rate)
if added > 0:
self.tokens = min(self.capacity, self.tokens + added)
self.last_refill = now
def request(self, n: int) -> str:
self._refill()
if self.tokens >= n:
self.tokens -= n
return f"grant({n})"
return "deny"
def add_tokens(self, k: int) -> None:
self.tokens = min(self.capacity, self.tokens + k)_refill이 State Box에 없었다는 점에 유의하라. 시간은 Black Box나 State Box에 존재하지 않는다. 이 모델들은 add_tokens가 호출되면 Token이 마법처럼 나타난다고 가정한다. Clear Box가 그 간극을 메워야 한다.
대부분의 버그는 여기에 산다. State Box는 tokens이 k만큼 늘어난다고 말한다. Clear Box는 Continuous Refill과 Capacity Cap도 처리하면서 State Box를 준수해야 한다.
Cleanroom이 테스트를 실행하지 않고도 정확성을 증명하는 방법
Cleanroom에서는 Clear Box에 대한 Unit Test를 작성하지 않는다. 대신 Verification을 수행한다.
각 Control Structure에 대해, 실행 전후에 참이 되어야 하는 Predicate을 쓴다. Sequence S1; S2의 경우, S1의 Postcondition이 S2의 Precondition을 함의함을 증명한다. if-then-else의 경우, 양쪽 Branch가 전체 Postcondition을 만족함을 증명한다. while 루프의 경우, Invariant를 찾아 Entry 시에 성립하고 각 Iteration에서 보존되며, 루프 종료 시 원하는 Postcondition을 함의함을 증명한다.
이것은 Proof Assistant가 아니다. 연필과 종이다. 재귀 Function이 종료함을 비형식적으로 주장해 본 적이 있다면, 이미 Cleanroom 증명의 90퍼센트를 한 셈이다.
왜 대부분의 팀이 이것을 사용하지 않는가
뻔한 반대 의견은 시간이다. Black Box, State Box, 수작업 Proof을 작성하는 것이 코드를 쓰고 버그를 고치는 것보다 느린 것처럼 들린다.
IBM에서 Cleanroom을 개발한 Harlan Mills는 반대 결과를 측정했다. Cleanroom 팀은 대조 팀보다 한 자릿수 적은 결함으로 코드를 전달했고, 총 개발 시간은 디버거에서 거의 시간을 쓰지 않아서 더 짧았다.
덜 뻔한 반대 의견은 문화적이다. Box Structure는 타이핑하기 전에 생각하도록 강제한다. 대부분의 개발자는 이것을 불편해한다. Specification은 관료주의처럼 느껴진다. 아니다. 그것이 Design이다. Cleanroom에서 Design은 검증할 만큼 정밀한 표기법으로 쓰이며, 첫 구현 초안이 무시하는 다이어그램이 아니다.
Box Structure의 오버헤드가 값어치 있는 순간
모든 Utility Function을 이런 식으로 지정할 필요는 없다. Box Structure가 빛나는 곳은 버그 비용이 Specification 작성 시간보다 큰 곳이다: Payment Processing, Authorization, Distributed Consensus, Protocol, Workflow Engine 등. 또한 같은 유형의 버그를 반복해서 Production에 내보내고 테스트에서는 절대 잡지 못하는 팀에도 도움이 된다.
가볍게 시작하는 방법
Cleanroom 프로세스 전체를 도입할 필요는 없다. Box Structure 아이디어를 단일 모듈에 빌려 써라.
Production에서 문제를 일으킨 Function을 고른다. 그것의 Black Box를 쓴다: Input, Condition, Expected Output의 테이블이다. 기존 코드를 보지 마라. 실제로 하는 것이 아니라, 해야 할 것을 써라.
그 다음 State Box를 써라. 어떤 State가 필요한가? 각 Input이 그 State를 어떻게 변환하는가? 구현과 비교해 보라. 차이가 나는 곳이 버그나 문서화되지 않은 Assumption을 찾은 곳이다.
다음은 Python로 작성한 최소 Template이다.
"""
Black Box Specification: Rate Limiter
Stimuli: request(n), add_tokens(k)
History: sequence of all stimuli received
Rules:
1. After any sequence of stimuli, tokens available =
sum(add_tokens.k) - sum(grant.n)
2. request(n) grants iff tokens available >= n
3. tokens available never exceeds capacity
State Box Refinement:
State: tokens (integer, 0 <= tokens <= capacity)
Invariant: tokens accurately represents available tokens
"""
class TokenBucket:
"""Clear box implementation of the rate limiter state box."""
def __init__(self, capacity: int):
self.capacity = capacity
self.tokens = capacity
def request(self, n: int) -> str:
if n <= 0:
raise ValueError("request must be positive")
if self.tokens >= n:
self.tokens -= n
return f"grant({n})"
return "deny"
def add_tokens(self, k: int) -> None:
if k < 0:
raise ValueError("cannot add negative tokens")
self.tokens = min(self.capacity, self.tokens + k)Comment가 Specification이다. Code가 Implementation이다. 같은 파일에 두면 Refinement가 가시적이고 Review 가능해진다.
진정한 가치는 관심사의 분리에 있다
Box Structure는 마법이 아니다. 모든 버그를 잡지는 못한다. 그것이 하는 일은 대부분의 개발 프로세스가 건너뛰는 규율을 강제하는 것이다. 구축하기 전에 “올바름”이 무엇인지 정의하는 것.
Black Box는 모듈의 Contract와 내부를 분리한다. State Box는 Data Model과 코드를 분리한다. Clear Box는 Implementation과 Proof를 분리한다. 각 겹은 하나의 역할을 맡고, 다음으로 넘어가기 전에 검증한다.
그래서 신경 써야 한다. “해야 할 일”과 “실제로 하는 일” 사이의 틈이 당신의 버그가 사는 곳이며, Box Structure는 단 하나의 테스트도 쓰기 전에 그 틈을 메우는 체계적인 방법이다.
더 깊이 알고 싶다면 Mills의 『Cleanroom Software Engineering』과 원래의 IBM Technical Report가 여전히 가장 명확한 참고 자료다. 아이디어는 오래되었다. 그것이 막는 버그는 그렇지 않다.