나는 코그와 이드리스 같은 언어가 어떻게 그 언어로 작성된 프로그램의 특성을 증명할 수 있는지를 이해한다. (주제에 대한 나의 작은 경험으로 판단해라.) 그러나 나는 외부에서 같은 것을 할 수있는 친숙한 방법이 있는지 궁금하다. 이미 존재하는 코드베이스.내 C++ 프로그램에 대한 속성을 증명할 방법이 있습니까?
C++로 작성된 알고리즘의 정확성을 증명하기 위해 Coq 또는 다른 특수 도구와 같은 도구를 사용할 수있는 방법이 있습니까? 그렇다면 그렇게하기위한 요구 사항은 무엇입니까?
"속성 증명"이 의미하는 바에 달려 있습니다. 내가 아는 한, C 프로그램의 간단한 속성을 검사하기위한 정적 분석 도구가 많이 있으며, 표현력, 사용 편의성, 분석의 건전성 등에서 광범위합니다. 일반적으로 프로그램이 무료인지 확인하는 데 사용됩니다 런타임 오류가 있지만 완전한 기능 사양을 확인하는 데는 그리 좋지 않습니다. 이러한 유형의 속성의 경우 자동으로 선택하지 않고 직접 증명을 수동으로 작성해야하는보다 강력한 증명기에 의존해야 할 수 있습니다.
Coq에 대해 언급 했으므로 C 프로그램을 검증하기위한 두 개의 Coq 기반 도구 (C++에서는 작동하지 않음)를 참조하고자합니다. 후자의 범주에는 Verified Software Toolchain이라는 논리가 있습니다. Coq 내부에 내장 된 C 프로그램에 대한 추론. 프로그램의 동작에 대한 증거를 작성하고 프로그램이 기능 사양을 충족하는지 보여주는 것을 포함하여 Coq가이를 확인하도록 할 수 있습니다. 이전 범주에는 런타임 오류가 없는지 프로그램을 검사하는 자동 정적 분석 도구 인 Verasco이 있습니다. 이 도구의 한 가지 좋은 점은 그 자체가 검증 된 프로그램이므로 제공하는 분석에 대해 추가로 확신을 가질 수 있음을 의미합니다.
기타 흥미로운 도구로는 위의 설명에서 언급 한 Frama-C과 Microsoft의 정적 분석기 VCC이 있습니다. 그러나 C++에서는 작동하지 않습니다.
C의 경우 [Frama-C] (http://frama-c.com/)가있어 프로그램의 동작을 추론합니다. 코드 알고리즘 코드가/compilable with C와 호환되면이를 사용할 수 있습니다. –