✅ 요약

정적 분석의 soundness는 논리학적 soundness 개념을 “프로그램 의미론”에 적용한 것이라고 볼 수 있습니다.

• 논리학: 증명 체계 ↔ 모델 이론

• 정적 분석: 추상 의미론 ↔ 구체 의미론

  → 틀린 결론은 절대 내리지 않는다는 보장을 공유.

1. First-Order Logic에서의 Soundness

• 정의 추론 규칙이나 증명 체계(proof system)가 sound하다는 것은, 그 체계에서 증명 가능한 모든 명제가 실제 의미론(모델)에서도 참이라는 것.

• 형식화

  $$ \vdash \varphi \;\;\Rightarrow\;\; \models \varphi $$

  즉, 증명(provability) → 참(semantic truth) (모든 증명 가능한 문장은 실제 모델에서 참이다.)

• 의미

  • 논리 체계가 sound하다는 건 “틀린 것을 증명하지 않는다”는 보장.
  • 다만, 참인 모든 것을 증명할 수 있는지는 보장하지 않음 (그건 completeness 문제).

2. 정적 분석(Static Analysis)에서의 Soundness

• 정의 정적 분석이 sound하다는 것은, 추상 의미론(abstract semantics)이 구체 의미론(collecting semantics)을 과잉근사(over-approximation) 한다는 것.

• 형식화 프로그램 P, 추상화 함수 $\alpha$, 구체 의미론 $\llbracket P \rrbracket_C$, 추상 의미론 $\llbracket P \rrbracket_A$에 대해:

  $$ \alpha(\llbracket P \rrbracket_C) \;\;\subseteq\;\; \llbracket P \rrbracket_A $$

  즉, 추상 의미론은 실제 도달 가능한 모든 상태를 포함해야 한다.

• 의미

  • 분석 결과가 놓치는 실제 실행은 없어야 함.
  • 따라서 안전 성질(safety property) 검증에 쓸 수 있음.
  • 하지만 필요 없는 실행을 포함할 수 있어서 false alarm은 발생 가능.

3. 연관성

• 형식적 구조
  • 논리학에서: 증명 시스템이 의미론을 sound하게 근사.
  • 정적 분석에서: 추상 의미론이 구체 의미론을 sound하게 근사.
• 공통된 철학
  • “우리가 도출한 결론은 틀리지 않는다”는 안정성 보장.
  • 대신, 불완전성(모든 참을 증명 못함 / false alarm 발생)은 감수.
• 추상 해석(Abstract Interpretation) 자체가 논리학적 아이디어(모델과 증명 사이의 관계)에서 영감을 받아 “구체 의미론과 추상 의미론 사이의 관계”를 정의한 것.

4. 비유