Program Correctness & Verification

1. Overview

프로그램 정확성 검증(Program Correctness & Verification, PCV)은 내가 짠 코드 덩어리가 "입력 데이터에 대해 예상한 출력을 단 0.1%의 오차도 없이 뱉어내는가?"를 수만 번의 테스트 케이스 실행이 아닌, 단 한 장의 수학적 연역 논리로 완벽히 증명해 내는 '알고리즘 물리학'입니다.

학습자는 코드의 윗줄과 아랫줄 사이에 성립해야 하는 수학적 제약 조건(Pre-condition, Post-condition)을 명시하는 **호어 논리(Hoare Logic)**를 뜯어보고, while 루프가 도는 와중에도 절대 깨지지 않는 불변의 진리인 **루프 불변성(Loop Invariants)**의 수리적 역학을 해부합니다. 나아가 재귀(Recursion)나 무한 루프가 영원히 돌지 않고 반드시 종료(Termination)됨을 정렬(Well-founded) 관계로 증명하며, 미션 크리티컬(의료기기, 항공우주) 소프트웨어가 결함 제로를 보장하는 극한의 무결성 아키텍처 능력을 확보합니다.

2. Scope & Boundaries

In-Scope

• 호어 논리 물리 (Hoare Mechanics): 사전 조건(Pre-condition, $P$), 사후 조건(Post-condition, $Q$), 호어 트리플(Hoare Triple, $\{P\} C \{Q\}$).
• 공리적 의미론 (Axiomatic Semantics): 할당 공리(Assignment Axiom), 조건문 규칙(Conditional Rule), 시퀀스 합성 규칙(Composition Rule).
• 루프의 수리적 해부 (Loop Physics): 루프 불변성(Loop Invariant, $I$), 유지성(Maintenance), 부분 정확성(Partial Correctness).
• 종료성 증명 (Termination & Total Correctness): 부분 정확성 + 루프 종료(Termination) = 완전 정확성(Total Correctness), 바운드 함수(Bound Function), 정초 관계(Well-founded Relation).

Out-of-Scope

• 시스템 아키텍처 단위의 동시성 증명: 스레드 2개가 경합을 벌일 때 발생하는 데드락 증명 → 01-02-03. Formal Specifications & TLA+ 영역.
• 화이트박스/블랙박스 유닛 테스트 기법: 경계값 분석(Boundary Value)이나 분기 커버리지(Branch Coverage) 같은 QA 기법 → 09-04. QA & Quality Assurance 영역.

Boundaries

• PCV vs. Testing (09-04): 소프트웨어 테스팅(09-04)이 "벌레(Bug)가 있는지 여기저기 찔러보는 귀납적 낚시"라면, PCV는 "이 웅덩이에는 애초에 벌레가 물리적으로 존재할 수 없음을 수식으로 못 박아버리는 연역적 결계"입니다.

3. Counterexample

• 루프 불변성 누락의 배열 폭발 (Loop Boundary Fallacy): 이진 탐색(Binary Search) 코드를 짜면서 low <= high 루프 안의 mid = (low + high) / 2 계산식만 집중할 뿐, 매 반복(Iteration)마다 "찾고자 하는 값은 반드시 [low, high] 구간 내에 존재한다"는 루프 불변성($I$)을 수학적으로 세우지 않는 행위. 오프 바이 원(Off-by-one, low = mid인지 low = mid + 1인지) 에러로 인해 배열 범위를 초과(Out of Bounds)하여 메모리 세그먼테이션 폴트가 터지는 건, 루프 진입 전/중/후의 불변성이 깨졌기 때문입니다.
• 종료 조건 증명 부재 (Non-termination Fallacy): while(x != 0)이라는 루프를 짜놓고 $x$ 가 홀수일 때 2를 빼고 짝수일 때 3을 더하는 짓을 하면서 루프가 알아서 언젠가 끝나겠지 착각하는 무지. 감소하는 바운드 함수(Bound Function)가 0을 향해 단조 감소(Monotonically Decreasing)함을 수리적으로 증명하지 않은 코드는, 우연히 조건이 빗맞을 경우 서버의 CPU 점유율을 100%로 쳐박는 무한 루프 폭탄이 됩니다.

4. Prerequisites

• 명제 및 술어 논리 (Basic): 사전 조건과 사후 조건을 $P(x) \land (y > 0)$ 같은 술어 논리로 작성하고 조작해야 하므로 필수적입니다. (01-02-01 PPL)

5. Learning Map

6. Learning Topics

Basic

Core Topic 01: 호어 논리와 계약 주도 프로그래밍 (Hoare Triples)

• Why to Learn: 함수 하나를 짜더라도 호출자가 보장해야 할 입력(Pre)과 내가 책임질 출력(Post)의 선을 수학적으로 긋기 위해서입니다.
• What to Learn:
  • Concepts: 사전 조건(Pre-condition, $P$), 사후 조건(Post-condition, $Q$), 호어 트리플(Hoare Triple, $\{P\} C \{Q\}$).
  • Skills: 상태(State) 검증, 계약에 의한 설계(Design by Contract).
  • Tools: 코드 내 assert() 문.
  • Trade-offs: 모든 함수마다 $\{P\}$ 와 $\{Q\}$ 를 주석이나 assert로 떡칠해야 하는 타이핑 피로도 vs 이 계약이 한 번만 잘 설정되면 런타임에 에러가 났을 때 누구의 잘못(호출자 vs 구현자)인지 0.1초 만에 밝혀지는 디버깅의 신속성.
• How to Learn:
  • 1단계: $\{x > 0\} \; y = x + 1 \; \{y > 1\}$ 이라는 호어 트리플에서, $x$ 가 양수라는 사전 조건이 코드 y = x + 1의 물리를 거쳐 $y$ 가 1보다 크다는 완벽한 사후 조건으로 맵핑됨을 해부합니다.
  • 2단계: 사전 조건을 너무 느슨하게(Weak) 잡으면 함수 내부에서 예외 처리를 다 해줘야 하고, 너무 빡세게(Strong) 잡으면 함수 호출하기가 극도로 까다로워지는 아키텍처적 줄다리기를 뜯어봅니다.
• Implement: 나눗셈 함수 div(a, b)를 구현할 때 맨 윗줄에 사전 조건 assert(b != 0)과 맨 아랫줄에 사후 조건 assert(result * b == a)를 박아넣어, 계약이 깨질 시 크래시를 내는 계약 주도 함수 작성.

Recommended

Core Topic 02: 공리적 의미론과 가장 약한 사전 조건 (Axiomatic Rules & WP)

• Why to Learn: 내가 원하는 결과($Q$)를 얻기 위해, 코드($C$) 진입 전에 변수들이 어떤 상태여야 하는지($P$)를 수학 공식으로 거꾸로 역산해 내기 위함입니다.
• What to Learn:
  • Concepts: 할당 공리(Assignment Axiom), 가장 약한 사전 조건(Weakest Precondition, $wp(C, Q)$).
  • Skills: 조건문 규칙(if-else), 순차 합성 규칙(Sequence Composition).
  • Tools: 연역적 추론 시스템.
  • Trade-offs: 결과에서부터 거꾸로 역추적하여(Backward Chaining) 코드가 무조건 작동하는 최소한의 허들을 수학적으로 뽑아내는 우아함 vs 복잡한 객체 참조(Pointer)나 함수 호출이 끼어들면 수식이 뇌 용량을 초과해 버리는 연산 복잡도.
• How to Learn:
  • 1단계: 사후 조건 $Q: \{x > 5\}$ 와 할당문 $C: x = y + 2$ 가 주어졌을 때, $x$ 자리에 $y+2$ 를 치환하여 가장 약한 사전 조건 $wp$ 가 $y > 3$ 임을 기계적으로 도출해 내는 할당 공리를 해부합니다.
  • 2단계: if (B) C1 else C2 구문의 $wp$ 를 계산할 때, $(B \rightarrow wp(C1, Q)) \land (\lnot B \rightarrow wp(C2, Q))$ 라는 무자비한 명제 논리로 분해하여 CPU 브랜치의 물리적 양면성을 수학으로 증명합니다.
• Implement: 기호 연산 라이브러리(예: SymPy)를 이용해, 파이썬 할당문 문자열 "x = y + 2"와 사후 조건 수식 "x > 5"를 파싱한 뒤 역산하여 사전 조건 수식 "y > 3"을 뱉어내는 미니 WP 계산기 모듈 작성.

Practical

Core Topic 03: 루프 불변성과 부분 정확성 증명 (Loop Invariants)

• Why to Learn: 수십만 번 반복되는 루프 안에서 $i$ 와 $j$ 인덱스가 미쳐 날뛰더라도, 내가 짠 코드가 절대 정렬을 흩트리거나 메모리를 터트리지 않음을 머릿속으로 증명하기 위해서입니다.
• What to Learn:
  • Concepts: 루프 불변성(Loop Invariant, $I$), 부분 정확성(Partial Correctness).
  • Skills: 3단계 증명법(초기화 Initialization, 유지 Maintenance, 종료 증명 Termination/Post-condition).
  • Tools: 이진 탐색(Binary Search), 삽입 정렬(Insertion Sort) 알고리즘 분석.
  • Trade-offs: 어떤 강력한 불변성 공식을 찾아내기만 하면 루프 전체의 복잡도를 단 3줄의 귀납법으로 찌그러뜨리는 강력함 vs 정작 그 알맞은 불변성 식($I$)을 기계가 자동으로 찾아주지 못하고 인간의 통찰력에 의존해야 하는 휴리스틱.
• How to Learn:
  • 1단계: 배열의 원소를 다 더하는 루프에서 "현재 단계 $k$ 까지 $sum$ 변수 안에는 배열의 $0$ 부터 $k-1$ 까지의 합이 들어있다"라는 루프 불변성 $I$ 를 수립하고, 루프 한 바퀴($C$)를 돌았을 때 이 불변성이 유지됨($\{I \land B\} C \{I\}$)을 뜯어봅니다.
  • 2단계: 루프가 종료되는 순간 조건 $B$ 가 거짓이 되므로, $I \land \lnot B \implies Q$ (최종 사후 조건)로 자연스럽게 연결되는 톱니바퀴 같은 수학적 증명 구조를 해부합니다.
• Implement: 삽입 정렬(Insertion Sort) 1스텝마다 assert(is_sorted(arr[0:i])) 불변성 체크 함수를 강제로 박아넣어, 인덱스 오타로 인해 정렬이 깨지는 즉시 루프 불변성 위반 에러를 뿜게 하는 방어적 정렬 코드 작성.

Advanced

Core Topic 04: 종료성 증명과 완전 정확성 (Termination & Total Correctness)

• Why to Learn: 내 알고리즘이 "만약 끝난다면 올바른 답을 낸다(부분 정확성)"는 변명에서 벗어나, "무조건 끝난다(종료성)"는 것을 합쳐 시스템 멈춤(Hang)의 공포를 완전히 소거하기 위함입니다.
• What to Learn:
  • Concepts: 완전 정확성(Total Correctness = Partial Correctness + Termination).
  • Skills: 바운드 함수(Bound Function / Variant), 정초 관계(Well-founded Relation, 무한히 작아지지 않는 집합).
  • Tools: Halting Problem 한계 이해.
  • Trade-offs: while(true) 형태의 무한 대기 서버 로직에서는 종료성 증명이 의미가 없고 Safety(죽지 않음)만 중요한 비동기 패러다임 vs 반드시 유한한 시간 안에 답을 내고 죽어야 하는 배치 데이터 파이프라인(Batch Algorithm)에서의 완벽한 종료 보장.
• How to Learn:
  • 1단계: 정수 $N$ 에서 시작해 루프를 돌 때마다 $N$ 이 반드시 1 이상 감소하고, $N=0$ 이 되면 루프를 탈출하는 바운드 함수 $V(N)$ 을 설정하여 "정수는 무한히 쪼개질 수 없으므로 무조건 끝난다"는 정초성의 물리를 뜯어봅니다.
  • 2단계: 앨런 튜링의 '정지 문제(Halting Problem)' 증명을 통해, 임의의 프로그램이 멈출지 안 멈출지를 100% 알아내는 범용 알고리즘은 수학적으로 불가능하며, 인간 아키텍트가 직접 각 코드마다 바운드 함수를 짜내야만 하는 철학적 한계를 분석합니다.
• Implement: 재귀 깊이(Recursion Depth)나 루프 변수(Iteration Count)가 루프마다 단조 감소(Monotonically Decreasing)하는지 런타임에 추적하여, 값이 커지거나 변동이 없으면 무한 루프 가능성 폭발(Infinite Loop Panic)을 던지는 디버깅 트레이서 구현.

7. Terminology

8. References

Primary

• [P1] CS2023 - DS/Discrete Structures and Modeling — Foundations of verification.
• [P2] SWEBOK v4.0 - Software Quality / Verification — Industry quality standards.

Secondary

• [The Science of Programming] David Gries — Classic text on Hoare logic.
• [Formal Methods for Software Engineering] — Modern approach to PCV tools.

Industry

• [MISRA C Standards] — Correctness-focused coding rules for safety-critical.
• [Static Analysis Security Testing (SAST) Guides] — PCV in modern DevSecOps.

9. Final Checklist

Primary

• 주어진 코드 한 줄과 그 사후조건을 바탕으로, 해당 등식이 성립하기 위해 필요한 사전조건을 '호어 트리플' 규칙에 따라 유도 가능한가? (P1)
• 특정 루프 로직에서 불변량(Invariant)이 초기화 단계에서는 맞지만 유지 단계에서 깨지는 사례를 찾아 논리적 오류를 지적할 수 있는 가? (P1)

Secondary

• '부분 정당성' 증명이 '완전 정당성'으로 격상되기 위해 순위 함수(Ranking Function)가 물리적으로 어떤 역할을 수행해야 하는지 설명 가능한가?
• 정적 분석 도구가 잡아내는 'Potential Null Pointer' 오류가 PCV의 사전조건(Pre-condition) 검증과 어떻게 수학적으로 연결되는지 소통 가능한가?

Industry

• 항공우주나 의료용 소프트웨어와 같은 고신뢰 시스템 설계 시, 코드 작성 전 불변 조건을 먼저 설계하여 런타임 치명 결함을 0%로 수렴시키는 전략을 제안할 수 있는 가? (SFIA)
• 코드 리뷰 과정에서 주관적인 의견이 아닌, 호어 논리 기반의 데이터 흐름 분석을 통해 잠재적 엣지 케이스 버그를 수학적으로 증명하고 설득할 수 있는 가?