추상 불변식 생성기

무엇을 해주나

• 코드에서 명세가 필요한 지점(루프, 함수 경계, assert)을 먼저 찾아냅니다.
• 구간(interval)·관계(relational)·형태(shape) 분석을 통해 변수 범위와 변수 간 관계, 자료구조 속성을 추론합니다.
• 초기화·유지·종료 3조건을 만족하는 루프 불변식을 템플릿(카운터/누적/탐색 루프) 기반으로 생성합니다.
• 배열 접근, 나눗셈, 널 포인터 같은 전제조건과 정렬·최대값·이진탐색 같은 사후조건을 자동 제안합니다.
• 최종 결과를 Dafny, Isabelle/HOL, Coq, ACSL(C) 문법으로 바로 붙여 쓸 수 있게 포맷합니다.
• 약한 불변식 강화, 중첩 루프, 다중 탈출 조건 처리 패턴도 함께 제공합니다.

이런 분께 추천

• Dafny·Coq·Isabelle·Frama-C로 형식 검증을 하는 연구자·엔지니어
• 안전 필수(safety-critical) 코드에 계약(contract)을 붙여야 하는 임베디드/항공/금융 개발자
• 알고리즘 정확성 증명을 가르치거나 배우는 대학원생·강의자

활용 예시

1. 파이썬 삽입 정렬 코드를 붙여넣고 "Dafny 불변식으로 옮겨줘"라고 요청 → 외부/내부 루프 불변식과 multiset 보존 조건까지 포함한 Dafny 메서드를 받습니다.
2. C 함수 int find_max(int arr[], int n)에 대해 ACSL 주석(requires \valid(...), loop invariant, loop variant)을 생성해 Frama-C 검증에 투입합니다.
3. 검증기가 "invariant too weak"를 낼 때, 이미 처리한 인덱스 구간에 대한 속성을 추가하는 강화 기법을 적용해 증명을 통과시킵니다.

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

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

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