{log}: From a Constraint Logic Programming Language to a Formal Verification Tool

이 논문은 집합과 이진 관계를 1 등 시민으로 다루는 제약 논리 프로그래밍 언어 {log}가 상태 기계 기반의 명세 언어, 실행 환경, 검증 조건 생성기, 자동 검증 및 테스트 케이스 생성 기능을 갖춘 통합된 형식 검증 도구로 발전한 과정을 종합적으로 소개합니다.

핵심

이 논문은 **'Setlog'({log})**라는 컴퓨터 프로그램 언어가 어떻게 단순한 '코딩 도구'에서 '엄격한 검증 도구'로 진화했는지를 설명합니다.

비유하자면, 이 논문은 마치 '레고 블록'으로 만든 장난감 자동차가, 어떻게 '안전성 테스트를 통과한 실제 자동차'로 변신했는지에 대한 이야기입니다.

아래는 이 논문의 핵심 내용을 일상적인 비유로 풀어낸 설명입니다.

---

1. {log} 란 무엇인가? (레고와 수학의 만남)

처음에 {log} 는 **수학적인 집합 (Set)**과 **관계 (Relation)**를 다루는 특별한 언어였습니다.

• 기존의 상황: 보통 프로그래밍 언어는 "이런 기능을 하라"고 명령을 내리고, 검증 도구는 "그 기능이 맞는지 확인해라"고 따로 검사합니다. 마치 요리사 (개발자) 와 미식가 (검증자) 가 따로 일하는 것과 같습니다.
• {log} 의 특징: {log} 는 요리사이자 미식가를 동시에 합니다. 작성된 코드 자체가 "이렇게 만들어라 (프로그램)"이면서 동시에 "이게 맞다 (수학적 증명)"는 것을 의미합니다.
• 비유: 레고로 차를 만들 때, 조립 설명서 (코드) 를 쓰면 그 설명서 자체가 "이 차는 안전하다"는 증명서가 되는 셈입니다.

2. 문제점: 너무 자유로워서 위험해졌다

처음에는 이 자유로움이 좋았지만, 문제가 생겼습니다.

• 문제: 개발자가 너무 복잡한 레고 조각을 쓰거나, 수학적으로 증명할 수 없는 이상한 모양을 만들면, {log} 가 "이게 안전해?"라고 물어봐도 답을 못 합니다. (검증 불가)
• 결과: 코드를 작성하는 건 쉽지만, 그 코드가 정말 안전한지 확인하려면 사람이 직접 손으로 하나하나 증명해야 하는 번거로움이 생겼습니다.

3. 해결책: '상태 기계 (State Machine)'라는 새로운 규칙 도입

저자들은 {log} 에 **새로운 규칙 (언어 확장)**을 추가했습니다. 이를 **'상태 기계'**라고 부릅니다.

• 비유: 이제 레고를 조립할 때 "무조건 아무 모양이나 만들면 안 되고, 정해진 도면 (규칙) 에 맞춰서만 조립해야 한다"는 규칙을 도입한 것입니다.
• 효과:
  1. 자동화된 검사: 이 규칙에 맞춰 작성된 코드는 컴퓨터가 자동으로 "안전하다"고 증명해 줍니다.
  2. 실제 실행: 이 코드는 증명만 하는 게 아니라, 실제로 작동하는 프로그램 (프로토타입) 으로 바로 실행해 볼 수도 있습니다.
  3. 테스트 생성: 이 설계도 (코드) 를 보고, "어떤 상황에서 고장 날까?"를 미리 찾아내는 테스트 케이스를 자동으로 만들어줍니다.

4. 주요 기능 3 가지 (새로운 도구들)

이 논문은 {log} 에 세 가지 강력한 도구를 추가했다고 소개합니다.

① 자동 검사관 (VCG - 검증 조건 생성기)

• 역할: 개발자가 코드를 작성하면, 이 도구가 "이 코드가 항상 안전할까?"라는 질문 (검증 조건) 을 자동으로 만들어냅니다.
• 작동: {log} 가 이 질문에 대해 "네, 안전합니다 (증명 완료)" 또는 "아니요, 여기가 위험합니다 (반례 발견)"라고 답합니다.
• 비유: 자동차 설계도가 나오면, 컴퓨터가 자동으로 "브레이크가 미끄러운 길에서도 작동할까?"라는 시뮬레이션을 돌려주는 것과 같습니다.

② 실패 분석가 (Counterexample 분석)

• 상황: 만약 {log} 가 "이건 증명할 수 없어"라고 하면, 개발자는 당황합니다.
• 해결: {log} 는 단순히 "실패"라고만 말하지 않습니다. **"왜 실패했는지" 구체적인 이유 (반례)**를 보여줍니다.
  • 예: "아, 당신이 '빈 상자'를 넣으려 했을 때만 이 코드가 고장 나네요."
• 효과: 개발자는 이 정보를 보고 코드를 수정하면 됩니다. interactive(상호작용) 증명처럼 사람이 직접 증명할 필요 없이, 컴퓨터가 힌트를 줍니다.

③ 테스트 생성기 (TTF - 모델 기반 테스트)

• 역할: 설계도 (코드) 를 보고, "이 코드가 제대로 작동하는지 확인하기 위해 어떤 테스트를 해봐야 할까?"를 자동으로 찾아냅니다.
• 작동: 입력값의 모든 경우의 수를 나누어 (예: 빈 상자, 꽉 찬 상자, 섞인 상자 등) 각각의 상황에 맞는 테스트 데이터를 만들어냅니다.
• 비유: 자동차를 만들 때, "눈길, 비길, 모래길" 등 모든 상황을 시뮬레이션해서 테스트할 데이터를 자동으로 뽑아주는 로봇입니다.

5. 다른 도구들과의 차이점 (왜 {log} 인가?)

논문은 Agda, Dafny 같은 다른 유명한 검증 도구들과 비교합니다.

• 다른 도구들: 보통 '프로그램 언어'와 '검증 언어'가 분리되어 있거나, 외부의 강력한 수학 엔진 (SMT 솔버) 을 따로 불러와야 합니다.
• {log} 의 장점:
  • 하나의 언어: 프로그램, 설계도, 검증 조건이 모두 같은 언어로 씁니다.
  • 하나의 엔진: 실행, 증명, 테스트 생성을 모두 {log} 가 스스로 해결합니다. 외부 도구가 필요 없습니다.
  • 집합 (Set) 중심: 데이터의 집합과 관계를 자연스럽게 다루기 때문에, 복잡한 시스템의 로직을 표현하기 매우 직관적입니다.

6. 결론: 이론이 현실이 되다

이 논문은 단순히 이론적인 수학 논리를 소개하는 것이 아니라, 이론이 실제로 작동하는 강력한 도구로 완성되었음을 보여줍니다.

• 핵심 메시지: "우리는 {log} 라는 언어에 몇 가지 규칙과 도구를 추가해서, 개발자가 코드를 쓰면서 동시에 그 코드가 안전하다는 것을 자동으로 증명하고, 테스트까지 만들어내는 완벽한 통합 환경을 만들었습니다."

한 줄 요약:

"이제 개발자는 복잡한 수학 증명 없이도, 하나의 언어로 코드를 작성하고, 그 코드가 안전하다는 것을 자동으로 증명받으며, 필요한 테스트까지 자동으로 만들어내는 시대를 열었습니다."

기술 요약

논문 요약: {log}: 제약 논리 프로그래밍 언어에서 형식 검증 도구로

1. 개요 및 문제 제기

이 논문은 {log}(read 'setlog')라는 도구가 제약 논리 프로그래밍 (CLP) 언어에서 형식 검증 (Formal Verification) 환경으로 어떻게 진화했는지에 대한 종합적인 소개를 제공합니다.

• 문제점: 기존 {log}는 집합 (Sets) 과 이진 관계 (Binary Relations) 를 1 등 시민으로 다루는 선언적 프로그래밍 언어이자 집합 이론의 결정 절차 (Decision Procedures) 를 구현한 제약 충족 솔버였습니다. 그러나 프로그래머가 직접 검증 조건 (Verification Conditions, VC) 을 작성하고 솔버에 입력하여 속성을 검증하는 과정은 번거로웠습니다. 또한, 일반적인 프로그래밍 기능은 집합 이론의 결정 가능 부분 (Decidable Fragments) 을 벗어날 수 있어 자동 검증이 불가능한 경우가 많았습니다.
• 목표: 프로그래밍과 증명 (Specification & Proof) 을 통합하고, 동일한 코드가 프로그램이자 명세 (Specification) 가 되는 '프로그램 - 수식 이중성 (Program-Formula Duality)'을 유지하면서, 자동화된 형식 검증과 테스트 케이스 생성이 가능한 통합 환경을 구축하는 것입니다.

2. 방법론 및 핵심 기술

논문은 {log}를 기반으로 한 형식 검증 환경을 구성하기 위해 다음과 같은 방법론과 확장 기능을 도입했습니다.

2.1 상태 기계 (State Machine) 기술 언어

B 또는 Z 표기법과 유사하게, 집합 이론과 1 차 논리 (FOL) 를 기반으로 한 상태 기계 기술 언어를 {log} 위에 정의했습니다.

• 구조: 상태 변수 (State Variables), 불변식 (Invariants), 초기 상태 (Initial State), 연산 (Operations) 으로 구성됩니다.
• 특징: 재귀는 허용되지 않지만 (자동 검증 용이성 확보), 집합, 관계, 함수 및 그 연산자를 핵심 구성 요소로 사용합니다.
• 이중성: 동일한 코드가 실행 가능한 프로토타입 (프로그램) 이자 검증 대상 (명세) 으로 작동합니다.

2.2 Next 환경 (실행 및 분석)

• 기능: 결정론적이고 완전히 인스턴스화된 기능 시나리오 (Functional Scenarios) 의 실행과 분석을 단순화합니다.
• 작동 방식: 초기 상태와 연산을 순차적으로 연결 (>>) 하여 상태 전이를 추적하고, 각 단계에서 불변식 (Invariant) 을 자동으로 검사합니다.
• 장점: 명세 작성 초기 단계에서 오류를 발견하고 복잡한 상호작용을 분석하는 데 유용합니다.

2.3 기호 실행 (Symbolic Execution)

• 기능: 상수 대신 변수를 입력으로 사용하여 더 일반적인 결론을 도출합니다.
• 분석: {log} 솔버가 반환하는 제약 조건 (Constraints) 을 분석하여 모든 가능한 입력 값에 대한 시스템 동작을 검증합니다.

2.4 검증 조건 생성기 (VCG, Verification Condition Generator)

• 기능: 상태 기계 명세로부터 표준 검증 조건 (VC) 집합을 자동으로 생성합니다.
• 주요 VC:
  1. 초기 상태가 모든 불변식을 만족하는지 확인.
  2. 각 연산이 충족 가능 (Satisfiable) 하고 상태를 변경할 수 있는지 확인.
  3. 불변식 보조정리 (Invariance Lemmas): 각 연산이 모든 불변식을 보존하는지 확인.
• 해결 전략: 생성된 VC 를 {log} 솔버에 전달하여 자동 증명합니다. 증명 실패 시 반례 (Counterexample) 를 생성하여 사용자가 명세 오류나 누락된 가정 (Hypothesis) 을 파악하도록 돕습니다.

2.5 모델 기반 테스트 (TTF, Test Template Framework)

• 기능: {log} 상태 기계 명세로부터 테스트 케이스를 자동 생성합니다.
• 기법:
  • DNF (Disjunctive Normal Form): 연산의 전제 조건을 논리적 대안으로 분할.
  • SP (Standard Partitions): 집합 연산 (합집합, 교집합 등) 의 수학적 속성에 기반한 분할.
• 프로세스: 테스트 트리 (Testing Tree) 를 생성하고, {log} 솔버를 이용해 불만족 가능한 노드를 가지치기 (Pruning) 한 후, 잎 노드 (Leaves) 에서 구체적인 테스트 케이스 (Ground Solutions) 를 추출합니다.

2.6 결정 가능 부분 (Decidable Fragments)

{log}는 집합 이론의 여러 결정 가능 부분을 구현하여 자동 증명을 지원합니다.

• 핵심 이론: 유한 집합 대수, 관계 대수, 제한된 내포 집합 (RIS), 정수 구간, 선형 정수 산술 (LIA) 등.
• 제약: 집합 변수와 정수 변수가 혼합된 복잡한 식은 결정 불가능할 수 있으나, {log}는 특정 조건 (예: 제한된 양화사 사용) 하에서 자동 증명을 수행합니다.

3. 주요 기여 (Contributions)

1. 통합된 상태 기계 기술 언어: {log} 제약 언어 위에 정의된 선언적 상태 기계 기술 언어를 제공합니다.
2. Next 환경: 상태 기계 기반 기능 시나리오의 실행 및 분석을 간소화하는 인터랙티브 환경을 제공합니다.
3. 자동화된 VCG: 상태 기계에 대한 표준 검증 조건을 자동 생성하고, {log} 솔버를 통해 이를 해결하거나 실패 원인을 분석합니다.
4. 모델 기반 테스트 프레임워크: {log} 솔버를 백엔드로 사용하여 테스트 케이스를 자동 생성하는 TTF 를 구현했습니다.
5. 단일 언어 및 솔버: 프로그램, 명세, 속성, 테스트 생성에 모두 동일한 언어와 솔버를 사용합니다. 외부 솔버 (SMT 등) 가 필요하지 않습니다.

4. 결과 및 사례 연구

• 성공적인 적용: 'Birthday Book'(Spivey 의 예제) 을 포함한 여러 사례 연구를 통해 도구의 유효성을 입증했습니다.
• 자동화 효율성:
  • 중국 벽 (Chinese Wall) 보안 속성 검증에서 35 개 VC 중 30 개가 인간의 개입 없이 자동 해결되었습니다.
  • 착륙 장치 (Landing Gear) 시스템 모델 검증에서 60% 의 VC 가 1 차 실행에서 해결되었으며, 나머지도 최소한의 가정 추가만으로 해결되었습니다.
• 반례 분석: 증명 실패 시 생성된 구체적인 반례 (Counterexample) 를 통해 명세의 오류 (예: 누락된 전제 조건) 를 쉽게 파악할 수 있었습니다.

5. 의의 및 결론

이 논문은 CLP(제약 논리 프로그래밍) 기술이 함수형 프로그래밍 기반의 형식 검증 도구 (Agda, Dafny 등) 와 동등한 가치를 가질 수 있음을 보여줍니다.

• 혁신성:
  • 프로그램과 명세의 구분이 없는 단일 언어 접근법.
  • 외부 솔버 없이 내부 솔버 하나로 실행, 증명, 테스트 생성을 모두 처리.
  • 집합과 관계를 1 등 시민으로 취급하여 추상화 수준을 높임.
  • 완전 자동화 (Decision Procedures 기반).
• 향후 과제:
  • 검증 조건 증명 시 필요한 가정을 자동으로 찾는 기능 강화.
  • 정교한 정제 (Refinement) 증명 지원.
  • 결정 불가능한 영역에 대한 증명을 위해 외부 상호작용 증명기 (ITP) 와의 통합 및 하위 목표 처리 능력 향상.

결론적으로 {log}는 이론적 연구 (CLP 및 집합 프로그래밍) 를 실제 형식 검증 도구로 전환한 성공적인 사례이며, 소프트웨어의 신뢰성을 높이기 위한 통합된 접근 방식을 제시합니다.