Program Correctness & Verification

1. Overview

프로그램 정당성 및 검증(Program Correctness & Verification, PCV)은 코드가 단순히 "동작하는 것"과 "수학적으로 틀릴 수 없음을 보이는 것" 사이의 간극을 메우는 학문입니다.

학습자는 제어 흐름과 데이터 변화를 추적하는 호어 논리(Hoare Logic), 프로그램 상태를 고정하는 **사전 조건(Pre-condition)**과 사후 조건(Post-condition), 그리고 반복문의 무한 굴레 속에서도 유지되는 **루프 불변량(Loop Invariant)**의 개념을 배웁니다. 이를 통해 '운이 좋아서 안 터지는 코드'가 아니라, 모든 가능한 런타임 환경에서 논리적으로 완벽함이 입증된 고신뢰성 소프트웨어를 설계하고 검증하는 능력을 갖춥니다.

2. Scope & Boundaries

In-Scope

• Hoare Triple: $\{P\} C \{Q\}$ 형식의 선언적 정당성 분석 및 수리 증명
• Invariant Logic: 반복문($While$)과 재귀 로직의 물리적 변동성 제어
• Termination Proofs: 프로그램이 유한 시간 내에 반드시 종료됨을 입증하는 물리력(Ranking Functions)
• Static Contract Physics: 어설션(Assertion)과 불변 조건(Class Invariants)의 배치 기법

Out-of-Scope

• 런타임 디버깅 및 프로파일링 기술 (09-02 SDM 영역으로 위임)
• 특정 컴파일러의 최적화 정당성 (전문 컴파일러 공학 영역)

Boundaries

• PCV vs. Automated Testing: 테스트가 '실행 결과'를 관찰한다면, PCV는 '코드의 구조적 의미'를 기호 논리(Symbolic Logic)로 분석하여 실행 없이도 결함을 수학적으로 확정합니다.

3. Counterexample

• 단순히 "assert 문을 곳곳에 심는 것"은 PCV 학습이 아닙니다. 왜 특정 정렬 알고리즘의 **사후 조건(Post-condition)**에서 '데이터의 정렬됨'뿐만 아니라 '원래 집합의 보존(Permutation)'이 동시에 증명되어야 하는지 논리적 필요성을 설명하지 못하거나, 루프 불변량을 설정할 때 '반복문 종료 후의 상태'와 연결짓지 못한다면 PCV의 핵심을 놓치고 있는 것입니다.

4. Prerequisites

• 명제 및 서술어 논리 (Basic): 조건부 논리와 양화사 이해가 필수입니다. (02-01 PPL)
• Functions & Mappings (Recommended): 상태 전이를 함수적 사상으로 이해하기 위해 필요합니다. (01-02 FAM)

5. Learning Map

1. Assertion Anchoring: 코드 실행 전후에 지켜져야 할 수학적 약속(Contracts)을 정의합니다.
2. Step-by-Step Logic: 각 명령어 라인이 상태를 어떻게 변환하는지 논리 규칙을 적용합니다.
3. Inductive Loops: 변화하는 변수들 사이에서 '변하지 않는 진리'를 찾아 반복문을 격파합니다.
4. Total Correctness: 부분 정당증명을 넘어 프로그램의 '종료 보장'까지 물리적으로 입증합니다.

6. Learning Topics

Basic

Core: 호어 논리와 트리플 (Hoare Logic Basics)

• Why to Learn: 프로그램의 한 스텝이 일으키는 논리적 파급력을 수리적으로 추적하기 위함입니다.
• What to Learn:
  • 호어 트리플의 구조: $\{Pre\} Code \{Post\}$
  • 배정문(Assignment) 규칙: 역치환(Back-substitution)을 통한 조건 전파 물리
  • 부분 정당성(Partial Correctness)의 정의와 한계
• How to Learn:
  • x = x + 1과 같은 단순 코드의 사후 조건을 보고 적합한 최약 사전 조건(Weakest Precondition) 유도 실습
  • 조건문(If-Then-Else) 분기에서 두 경로의 사후 조건이 어떻게 통합되는지 논리 합(OR)으로 분석
• Implement: 특정 코드 블록과 사전 조건을 입력받아 논리적으로 도출되는 사후 조건을 산출하는 검증 틀

Recommended

Core: 루프 불변량과 귀납 증명 (Loop Invariants)

• Why to Learn: 복잡한 반복 로직이 모든 회차에서 의도대로 동작함을 수학적으로 확신하기 위해서입니다.
• What to Learn:
  • 루프 불변량의 3대 요건: 초기화(Initialization), 유지(Maintenance), 종료(Termination)
  • 인덱스 변수와 데이터 상태 사이의 물리적 연결 고리 찾기
  • 수학적 귀납법을 이용한 루프 무결성 입증 시퀀스
• How to Learn:
  • 이진 탐색(Binary Search) 알고리즘에서 left <= right 관계가 어떻게 불변량으로 작용하는지 정밀 분석
  • 단순 배열 합계 계산 로직의 불변량을 정의하고, 반복이 끝났을 때 결과가 정답과 일치함을 논리적으로 소통
• Implement: 루프 불변량을 주석으로 명시하고 이를 기반으로 런타임 체크를 수행하는 계약 기반 코드

Practical

Core: 프로그램 종료와 순위 함수 (Program Termination)

• Why to Learn: 무한 루프나 재귀 깊이 초과로 인한 시스템 다운을 물리적으로 예방하기 위함입니다.
• What to Learn:
  • 완전 정당성(Total Correctness) = 부분 정당성 + 종료 보장
  • 순위 함수(Ranking Function): 루프가 실행될 때마다 반드시 감소하는 양의 정수 값 모델링
  • 재귀 호출의 기저 사례(Base Case) 도달 가능성 증명
• How to Learn:
  • 유클리드 호제법 알고리즘에서 나머지 값이 루프마다 줄어들어 결국 0이 됨을 수학적으로 기술 실습
  • 복잡한 재귀 함수가 특정 입력 집합에서 반드시 유한 단계 내에 끝나는지 'Well-founded relation' 관점에서 탐구
• Implement: 재귀 호출 시 깊이를 제한하거나 종료 조건을 수리적으로 강제하는 안전 장치 모듈

Advanced

Core: 자동 검증 도구와 정적 분석 (Automated Verification)

• Why to Learn: 인간의 실수를 넘어 기계적인 엄밀함으로 대규모 코드 베이스의 무결성을 확보하기 위해서입니다.
• What to Learn:
  • 정적 분석(Static Analysis)의 물리적 한계: 라이스 정리(Rice's Theorem)와 불확정성
  • 심볼릭 실행(Symbolic Execution): 변수를 상수가 아닌 기호로 취급하여 모든 경로를 동시에 탐색
  • 모델 기반 검증과 코드 자동 생성의 논리 연결
• How to Learn:
  • 오픈소스 정적 분석 도구(SonarQube, ESLint 보안 플러그인 등)의 탐지 논리가 어떤 PCV 원칙을 쓰는지 분석
  • Dafny나 Coq와 같은 정형 검증 언어를 맛보며 코드를 짜는 동시에 증명을 병행하는 패러다임 연습
• Implement: 특정 조건(예: 0으로 나누기 방지)에 대해 코드 전체를 스캔하여 위반 지점을 찾는 미니 정적 분석기

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)
• 코드 리뷰 과정에서 주관적인 의견이 아닌, 호어 논리 기반의 데이터 흐름 분석을 통해 잠재적 엣지 케이스 버그를 수학적으로 증명하고 설득할 수 있는 가?