나는 C 프로젝트 몇 개를 작업 중이며 자동화 된 정리 이론을 사용하여 코드의 유효성을 검사하고 싶습니다. 이상적으로는 ATP를 사용하여 함수 계약의 유효성을 검사하고 싶습니다. 디자인/계약 스타일 코딩을 가능하게하는 C/gcc 또는 외부 소프트웨어/패키지/등의 기능이 있습니까?자동 정리에 사용하기 위해 계약 C로 디자인하기. 증명.
그렇다면 나만의 인센티브가 시작됩니다.
내 참조는 MSR의 SpeC# 또는 Sing #과 같지만 오픈 소스 사용자이고 오픈 소스 솔루션을 찾고 있습니다.
당연히 언어에 내장되어 있지는 않지만 추가 기능이 많이 있습니다. 대부분은 베타 버전입니다.하지만 자신 만의 것을 시작하기보다는 기여하는 것을 고려해보십시오.
RubyForge에서 제공되는 Design by Contract for C은 매우 유망 해 보입니다. GNU Nana은 오랫동안 사용되어 왔으며 아마도 사용자의 요구에 잘 맞을 것입니다. 희망이 도움이됩니다.
편집 : C를위한 디자인으로 계약에 this article at O'Reily를 체크 아웃 : 어설 션()와 계약에 의해 디자인에 대한 흥분 와
만족하지, 난에 대한 계약 구현에 의해 내 자신의 디자인을 만드는 데 착수 C. 일부 해결책을보고 난 후 을 Java 용 1으로 변경했습니다. 계약 제한을 표현하기 위해 객체 제한 언어의 하위 집합을 사용했습니다 [4]. Ruby와 Racc를 사용하여 Contract을 C for Contract로 만들었습니다.이 코드 생성기 은 계약을 확인하기 위해 C 주석에 포함 된 계약을 C 코드에 포함시킵니다.
정리 해설자를 사용하여 C 코드의 유효성을 검사하려면 VCC project을 확인해야합니다. 해당 웹 페이지에서 :
VCC는 동시 C 프로그램의 기계적 확인 프로그램입니다. VCC는 함수 사양, 데이터 불변 값, 루프 불변 및 유령 코드가 주석 처리 된 C 프로그램을 사용하고이 주석을 정확하게 증명하려고 시도합니다. . 성공하면 VCC는 귀하의 프로그램이 실제적으로 을 충족시킬 것이라고 약속합니다.
VCC는 Microsoft Research에서 매우 성숙한 시스템이며, Microsoft Hyper-V의 하이퍼 바이저를 확인하는 데 사용되었습니다. VCC도 오픈 소스입니다.