Program Verification프로그램 검증

호어 삼중항(Hoare Triple):
  {P} C {Q}
  P: 사전 조건(Precondition)
  C: 명령(Command)
  Q: 사후 조건(Postcondition)

의미: 실행 전 P가 참이면 C 실행 후 Q가 참

대입 공리:
  {P[x := e]} x := e {P}

순차 실행:
  {P} C₁ {R}   {R} C₂ {Q}
  ─────────────────────────
  {P} C₁; C₂ {Q}

조건문:
  {P ∧ B} C₁ {Q}   {P ∧ ¬B} C₂ {Q}
  ────────────────────────────────────
  {P} if B then C₁ else C₂ {Q}

반복문(루프 불변식):
  {I ∧ B} C {I}
  ────────────────────────────────
  {I} while B do C {I ∧ ¬B}

# 팩토리얼 계산 프로그램
# {n >= 0}
result = 1
i = 0
# 루프 불변식: result = i!  AND  0 <= i <= n
while i < n:
    i = i + 1
    result = result * i
# {result = n!}

증명:
- 초기화: i=0, result=1=0! ✓
- 유지: i→i+1, result→result*(i+1) = i!*(i+1) = (i+1)! ✓
- 종료: i=n → result = n! ✓

wp(x := e, Q) = Q[x := e]
wp(C₁;C₂, Q) = wp(C₁, wp(C₂, Q))
wp(if B then C₁ else C₂, Q)
  = (B → wp(C₁,Q)) ∧ (¬B → wp(C₂,Q))

예: wp(x := x+1, x>5) = x+1>5 = x>4