함수의 계약을 작성하기
전제조건은 함수 호출 전에 만족해야 할 조건이고 사후조건은 그 조건에서 반환 결과가 만족해야 할 관계다. 실행 예제를 여러 개 나열하기보다 허용한 입력 전체에 대한 성질을 기술한다. 하지만 명세가 실제 요구와 다르면 증명이 성공해도 원하는 동작을 확인하지 못하므로 계약 자체를 검토한다.
컴파일과 증명 구분
Rust 코드를 Why3 계열의 중간 검증 언어인 Coma로 옮기고 생성된 검증 조건을 증명기로 처리한다. 이 단계를 나누어 실행할 수도 있다. 변환에 성공한 결과와 조건을 증명한 결과는 서로 다르다. 증명하지 못한 경우에는 도구의 한계나 명세 부족 및 실제 코드 문제를 구분해 조사한다.
실패 조사와 환경
자동 증명으로 해결하지 못한 조건은 Why3 IDE에서 살펴볼 수 있다. 이전 증명 결과를 재사용하는 흐름에서는 현재 코드와 생성 자료가 맞는지도 확인한다. Rust와 검증용 라이브러리 및 증명 도구의 구성이 함께 맞아야 한다. 검증한 함수의 계약이 외부 연동이나 운영 환경 전체의 동작까지 자동으로 보장하는 것은 아니다.