ACSL 형식 명세 주석 도우미

무엇을 해주나

• C/C++ 함수에 ACSL 함수 계약(requires/ensures/assigns)을 작성합니다.
• 반복문에 루프 불변식(loop invariant), 종료 증명용 변형식(loop variant), loop assigns를 추가합니다.
• 포인터 유효성(\valid, \valid_read), 별칭 없음(\separated) 등 메모리 안전성 명세를 생성합니다.
• 재사용 가능한 술어(predicate)와 공리(axiomatic) 정의, 중간 assert/assume 삽입을 도와줍니다.
• 함수 분석 → 계약 작성 → 루프 주석 → 단정문 → 술어 정리의 5단계 워크플로를 따릅니다.
• references/ 폴더에 ACSL 문법 레퍼런스, 자주 쓰는 패턴, Frama-C 연동 팁이 동봉되어 있습니다.

이런 분께 추천

• Frama-C WP 플러그인으로 C 코드를 형식 검증하는 개발자·연구자
• 항공·자동차·의료 등 고신뢰 임베디드 소프트웨어 인증 작업자
• 배열 범위 초과, 널 포인터, 오버플로를 증명 수준에서 막고 싶은 팀
• 형식검증 수업·논문 실험에서 명세 작성 시간을 줄이고 싶은 학생

활용 예시

1. "이 find_max_index 함수에 ACSL 계약과 루프 불변식을 붙여줘" → 사후조건에 최댓값 성질까지 포함한 명세 생성
2. "memcpy 래퍼에 메모리 안전성 명세를 추가해줘" → \valid, \valid_read, \separated, assigns 절 작성
3. "입력이 음수일 때와 정상일 때를 나눠 behavior 명세로 만들어줘" → complete behaviors; disjoint behaviors;까지 포함한 분기 명세 생성

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

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

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