17
인증 된 프로그램을 설계하는 데 Coq를 사용하는 방법에 대해 이야기하는 여러 연구 그룹과 적어도 한 권의 책을 봅니다. 인증 프로그램의 정의에 대한 합의가 있습니까? 제가 말할 수있는 것에서는, 그것이 의미하는 바는 모두 프로그램이 합법적이고 정확한 타입임을 증명했습니다. 이제 프로그램의 유형은 비어 있고, 정렬되어 있고,> 5와 같은 요소가 포함되어 있다는 증거가있는 목록과 같이 정말 이국적인 것일 수 있습니다. 그러나 Coq가 보여준 인증 된 프로그램은 궁극적으로 총계 및 유형 안전성입니다. 모든 흥미로운 질문들이 마지막 유형에 포함 된 것으로 요약됩니다. wjedynak의 답변에 따라 1 인증 된 프로그램의 정의
편집, 나는 자비에 르로이의 종이 아래의 답변에 링크 된 "실제 컴파일러의 공식 확인"을 살펴했다. 나는 이것이 좋은 정보를 포함하고 있다고 생각하지만, Sandlin Blazy와 Xavier Leroy의 논문 Mechanized Semantics for the Clight Subset of the C Language에서이 일련의 연구에서보다 유익한 정보가 발견 될 수 있다고 생각합니다. 이것은 "형식 검증"보고서에 최적화가 추가 된 언어입니다. Blazy와 Leroy는 Clight 언어의 구문과 의미를 제시하고 5 장에서 이러한 의미의 유효성을 논의합니다. 5 장에서는 컴파일러 유효성 검사에 사용되는 다양한 전략 목록을 제공합니다. 공인 프로그램을 만들기위한 다양한 전략들. 이들은 다음과 같습니다 다른 의미 어떤 경우
와 의미의 특성
- 매뉴얼 리뷰
- , 아마이 있습니다 추가 할 수있는 포인트와 나는 더 많이 듣고 싶습니다.
인증 된 프로그램의 정의에 대한 원래의 질문으로 돌아가서, 나에게는 아직 조금 불명확합니다. Wjedynak 일종의 대답을 제공하지만, 사실 Leroy의 작업은 Coq에서 컴파일러를 만든 다음 어떤면에서는 그것을 증명하는 것과 관련이 있습니다. 이론적으로, 이제는 C-> Coq-> proof로 갈 수 있기 때문에 C 프로그램에 대한 것들을 증명할 수있게되었습니다. 우리가
- 가 X 언어로 COQ의 1 단계 또는 다른 증거 보조 도구에서 프로그램의 모델의
- 양식을하는 프로그램을 작성 수있는이 작업 흐름이처럼 그런 의미에서, 그것은 보인다. 이것은 Coq에서 프로그래밍 언어의 모델을 생성하거나 프로그램의 모델을 직접 생성 (즉, Coq에서 프로그램 자체를 다시 작성)하는 것과 관련 될 수 있습니다.
- 모델에 대한 몇 가지 속성을 입증하십시오. 어쩌면 그 값에 대한 증거 일 수 있습니다. 어쩌면 그것은 문장의 동등성을 입증 할 수 있습니다. (3 = 1 + 2 또는 f (x, y) = f (y, x)와 같은 것들입니다.)
- 그런 다음 이러한 증명을 바탕으로 원래 프로그램 인증 .
또한, 우리는 증거 보조 도구에서 프로그램의 사양을 만들 수 다음 사양에 대한 속성을 증명 있지만 프로그램 자체.
아무튼 나는 대체 정의가있는 경우 대체 정의를 듣는 것에 관심이 있습니다.
아주 유효한 질문입니다. 함수의 결과가 항상 이상하다는 것을 증명했다면, 이미이 함수가 정확하다는 것을 의미합니까? 나는 그렇지 않다. 내가 아는 바로는 사양은 문제의 모든 측면을 마지막 비트까지 설명하지 않습니다. 이는 "일부 측면 만 정확하다"고 말하는 것이 더 정확하다는 것을 의미합니다. 누구도 반대 할 것입니까? –