추상 도메인 탐색기

무엇을 해주나

추상 해석(abstract interpretation)을 이용해 코드를 실행하지 않고 변수의 값 범위와 변수 간 관계, 루프 불변식을 정적으로 추론합니다.

• 도메인 선택 가이드: Sign, Interval, Congruence, Octagon, Polyhedra, Reduced Product의 정밀도·비용 트레이드오프 표를 제공하고 목적에 맞는 도메인을 고르게 합니다.
• 6단계 분석 워크플로: 도메인 선택 → 초기 추상 상태 설정 → 전이 함수 적용(대입/조건/조인) → 루프 위드닝(∇)으로 종료 보장 → 내로잉(△)으로 정밀화 → 불변식 추출.
• 안전성 판정: 배열 인덱스 범위 초과, 0으로 나누기 가능성 등 위험 지점을 근사값 기반으로 보고합니다.
• 정직한 근사 표기: 근사값을 정확한 값처럼 말하지 않고 선택한 도메인의 한계(예: 옥타곤은 y = 2x를 표현 못함)를 함께 명시하도록 규칙화되어 있습니다.

이런 분께 추천

• 정적 분석·형식 검증·컴파일러 최적화를 공부하거나 연구하는 분
• 코드 리뷰 중 루프 불변식이나 변수 범위를 논리적으로 정리해야 하는 개발자
• 프로그램 분석 과목 과제나 논문 예제를 손으로 풀어보며 이해하고 싶은 학생

활용 예시

1. int x=0; while(x<10){x++; y--;} 코드를 넘기면 구간 도메인으로 루프 내부 x ∈ [0,9], 종료 시 x=10, y=90을 유도하고, 구간만으로는 x+y=100을 못 잡는다는 한계까지 설명합니다.
2. y = x*x; z = 100/y; 처럼 보이는 코드에서 부호 도메인으로 y ≥ 0을 얻고 y=0 가능성 때문에 0으로 나누기 위험이 있다고 판정합니다.
3. 이중 루프에서 옥타곤 도메인을 적용해 j ≤ i 같은 관계형 불변식을 뽑아내고, 더 복잡한 z = 3x 같은 선형 관계는 폴리헤드라로 넘어가야 함을 안내합니다.

이 파일의 지시를 읽고 그대로 따라서 나를 도와줘:
https://raw.githubusercontent.com/ArabelaTso/Skills-4-SE/HEAD/skills/abstract-domain-explorer/SKILL.md

내가 원하는 것: (여기에 하고 싶은 일을 쓰세요)

클로드스킬마트에서 찾은 스킬을 설치해줘.
GitHub 저장소 ArabelaTso/Skills-4-SE 의 skills/abstract-domain-explorer 폴더를 내 ~/.claude/skills/abstract-domain-explorer/ 에 그대로 복사해줘.
설치가 끝나면 이 스킬로 무엇을 할 수 있는지 한 줄로 알려줘.