Abstract Interpretation추상 해석

구체 의미론(Concrete):
  프로그램의 실제 모든 실행 상태 집합

추상 의미론(Abstract):
  구체 의미론을 "안전하게" 근사한 추상 값

구체 → 추상: 추상화 함수 α
추상 → 구체: 구체화 함수 γ

안전성(Soundness):
  실제 행동 ⊆ γ(추상 분석 결과)
  "실제 버그를 놓치지 않는다"

(C, ≤) ──α──→ (A, ⊑)
         ←──γ──

갈루아 연결 조건:
  ∀c ∈ C, a ∈ A:
  α(c) ⊑ a  iff  c ≤ γ(a)

⟹ α(γ(a)) ⊑ a   (추상화는 손실 가능)
   c ≤ γ(α(c))   (구체화-추상화는 안전)

부호 도메인:
  추상 값: {⊥, Neg, Zero, Pos, ⊤}
  γ(Pos) = {1, 2, 3, ...}
  γ(Neg) = {..., -2, -1}
  γ(⊤)   = 모든 정수

  추상 덧셈:
  Pos + Pos = Pos
  Neg + Neg = Neg
  Pos + Neg = ⊤   (모름)

구간 도메인 [l, u]:
  [2, 5] + [3, 7] = [5, 12]
  [2, 5] * [-1, 3] = [-5, 15]

8각형 도메인 (Octagon):
  ±x ± y ≤ c 형태의 제약
  변수 간 관계 포착

루프 분석:
  x = 0;
  while (x < 100) { x = x + 1; }

  구간 분석:
  반복 0: x ∈ [0,0]
  반복 1: x ∈ [0,1]
  반복 n: x ∈ [0,n]  ← 수렴 안 함!

  Widening (▽):
  [0,0] ▽ [0,1] = [0,+∞]  ← 강제 수렴
  이후 정제(Narrowing): [0,+∞] △ ... = [0,100]