ANSI/ISO C 사양 언어

이 문서에는 여러 가지 문제가 있습니다.개선을 돕거나 토크 페이지에서 이러한 문제에 대해 논의해 주십시오.(이러한 템플릿메시지를 삭제하는 방법과 타이밍에 대해 설명합니다) 이 글은 검증을 위해 추가 인용문이 필요합니다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선하는 데 도움을 주십시오. 조달되지 않은 자재는 제거될 수 있습니다.출처 : 'ANSI/ISO C 사양 언어'– 뉴스 · 신문 · 서적 · 학자 · JSTOR (2015년 2월) (이 템플릿 메시지 삭제 방법 및 삭제 시기 확인) 이 문서에는 일반적인 참조 목록이 포함되어 있지만 대응하는 충분한 인라인 인용이 없습니다. 좀 더 정확한 인용문을 도입하여 개선해 주시기 바랍니다. (2015년 2월) (템플릿 메시지 삭제 방법 및 삭제 시기 확인) (이 템플릿메시지를 삭제하는 방법과 타이밍을 확인합니다)

ANSI/ISO C 사양 언어(ACSL)는 Hoare 스타일의 사전 및 사후 조건과 불변성을 사용하는 C 프로그램의 사양 언어이며, 계약 패러다임을 따릅니다.사양은 C 프로그램에 대한 C 주석 주석으로 작성되며, 따라서 C 컴파일러와 함께 컴파일할 수 있습니다.

ACSL의 현재 검증 도구는 Frama-C입니다.또, C++ 용으로 정의된 자매 언어 ANSI/ISO C++ 사양 언어(ACSL++)도 실장하고 있습니다.

개요

1983년, 미국 국립 표준 협회(ANSI)는 C 언어를 표준화하기 위해 X3J11 위원회에 의뢰했습니다.C의 첫 번째 표준은 ANSI에 의해 발표되었다.이 문서는 이후 국제표준화기구(ISO)에 의해 채택되어 ISO에 의해 발행된 후속 개정판이 ANSI에 의해 채택되었지만 ANSI C라는 이름은 계속 사용되고 있습니다.

ACSL은 Behavioral Interface Specification Language(BISL; 행동 인터페이스 사양 언어)입니다.C 소스 코드의 동작 속성을 지정하는 것을 목적으로 합니다.이 언어의 주요 영감은 C 프로그램의 행동 속성의 연역적 검증을 위한 Caduceus 도구의 사양 언어에서 비롯됩니다.Caduceus의 사양 언어 자체는 Java 소스 코드의 유사한 목표를 목표로 하는 JML에서 영감을 받았습니다.

JML과의 한 가지 차이점은 ACSL은 정적 검증과 연역 검증을 지향하는 반면, JML은 ESC/Java 툴을 사용한 런타임 어설션 체크와 정적 검증을 모두 지향한다는 것입니다.

구문

다음 예제를 다음과 같은 함수의 프로토타입을 고려하십시오.incrstar:

/*@에는 \valid(p)가 필요합니다. @는 *p;를 할당합니다. @는 *p == \oldsup) + 1을 보증합니다. @*/ 무효 인크 (인트 *p); 

계약서는 다음과 같이 시작하는 코멘트로 제공됩니다./*@그 의미는 다음과 같습니다.

• 첫 번째 행은 전제 조건입니다.이 행은, 다음의 기능을 나타내고 있습니다.incrstar포인터로 호출해야 합니다.p안전하게 할당된 메모리 위치를 가리킵니다.
• 두 번째 줄은 frame 구로, 함수가incrstar메모리 위치는 변경되지 않지만,p.
• 마지막으로,ensures절은 post condition으로, 값은 다음과 같습니다.*p1씩 증가합니다.

상기 기능의 유효한 실장은 다음과 같습니다.

무효 인크 (인트 *p) {     (*p)++; } 

도구 지원

ACSL 의 기능의 대부분은, Frama-C 로 서포트되고 있습니다.

TrustInSoft 스태틱아나라이저는 Frama-C의 상용 파생 모델입니다.프로그램 동작을 확인하고 (언어 사양에 따라 내장된 규칙을 사용하여) 정의되지 않은 ^[1]동작의 인스턴스를 포착합니다.

레퍼런스

• VMCAI 2008 페이지 188 ~202의 ACSL 사용률 모듈러 어설션체크를 위한 충분한 전제 조건의 예
• 예를 들어 ACSL은 단순 알고리즘의 ACSL 규격에 대한 잘 문서화된 모음으로 Fraunhofer FOKUS의 검증 그룹에 의해 개발 및 유지된다.
• WP와 ACSL을 사용한 Frama-C에 대한 튜토리얼로, 툴의 배후에 있는 이론에 대한 아이디어도 제공합니다(프랑스어로도 이용 가능).
• DO-178C 준거 프로젝트의 맥락에서 ACSL 및 Frama-C를 사용하여 낮은 수준의 요건을 책정 및 검증하는 것에 관한 보고서
• [ 1 ] 、 「 「 」 、 「 」 、 「 」 、 「 」 、 「 」 、 「 」 에서의 ACSL 의 사용에 대해 기술한 리포트.
• Techikum Wien ACSL 및 Frama-C에서는 설계 및 검증에 관한 코스를 수강하고 있습니다.

외부 링크

• 완전한 ACSL 사양은 Frama-C 다운로드 페이지에서 확인할 수 있습니다.
• TrustInSoft의 TSnippet을 사용하면 ACSL을 사용하여 브라우저 내에서 C 스니펫을 테스트할 수 있습니다.