---
title: "명세 없이도 정제(Refinement)를 이해할 수 있다 — DB 마이그레이션으로 설명하는 형식 검증"
published: 2026-01-20T22:18:03.000Z
canonical: https://jeff.news/article/1040
---
# 명세 없이도 정제(Refinement)를 이해할 수 있다 — DB 마이그레이션으로 설명하는 형식 검증

정형 명세의 핵심 개념인 정제(refinement)를 SQL 스키마 마이그레이션이라는 익숙한 맥락으로 풀어내는 글. boolean→timestamp→이벤트소싱 전환에서 레거시 코드 호환성을 정제 매핑으로 검증하는 과정을 보여준다.

- 정형 명세(formal specification)에서 쓰는 **정제(refinement)** 개념을 DB 마이그레이션이라는 익숙한 맥락으로 설명하는 글임. 핵심 주장은: 정제가 어렵게 느껴지는 이유가 개념 자체가 어려워서가 아니라, 형식 검증이라는 낯선 맥락에서 배우기 때문이라는 거임

- 첫 번째 예시: `user` 테이블에 `is_activated` boolean 컬럼이 있는데 이걸 nullable `activated_at` 타임스탬프로 마이그레이션하려 함. SQL 쿼리는 바꿀 수 있지만 그 결과를 쓰는 코드는 못 바꾸는 상황. 정제 매핑 `f(new_user)`를 정의해서 `activated_at`이 null이 아니면 `is_activated = true`로 변환하면, 레거시 코드가 이 매핑을 거쳐서 기존과 동일하게 동작함

- 두 번째 예시: 한 단계 더 나가서 이벤트 소싱 모델로 전환. `user_events` 테이블에 `(user_id, timestamp, event)` 레코드를 추가하는 방식. 여기서도 정제 매핑 `g(newer_user)`를 정의하면 체이닝이 가능해짐 — 정말 오래된 코드는 `f(g(newer_user))`로 돌리면 됨

- 여기서 재밌어지는 건 **변경 가능성 제약(mutability constraints)**을 추가할 때임. "한번 활성화되면 비활성화 불가"라는 제약 C1을 걸면:
  - `activated_at` 모델은 정제가 유지됨 (C2를 만족하면 C1도 만족)
  - 이벤트 소싱 모델은 정제가 **깨짐** — deactivation 이벤트를 추가할 수 있으니까
  - `activated_at` + `activated_until`을 쓰는 `bad_user` 모델도 깨짐 — 시간이 지나면 `activated`가 false로 바뀔 수 있으니까

- 결론: 정제 매핑이 DB 뷰(view)와 어떤 관계인지 생각해보라는 열린 질문을 던짐. 저자는 이걸 형식 검증 책에 넣고 싶어하는데, 이미 내용 추가하기엔 늦었을 수도 있다고 함

> [!TIP]
> 스키마 마이그레이션할 때 "이전 코드가 새 스키마에서도 동일하게 동작하는가?"를 정제 매핑으로 검증하는 프레임워크를 갖추면 브레이킹 체인지를 구조적으로 잡아낼 수 있음

## 핵심 포인트

- is_activated → activated_at → event sourcing 단계별 마이그레이션 예시
- 정제 매핑 f(), g()의 체이닝으로 레거시 코드 호환성 유지
- mutability 제약 추가 시 정제가 깨지는 조건 분석
- 정제 매핑과 DB view의 관계에 대한 열린 질문

## 인사이트

스키마 마이그레이션에서 브레이킹 체인지를 구조적으로 잡아내는 프레임워크로서 정제 개념이 실용적 가치가 있음.