실행 이전에 조건 확인하기
일부 입력을 직접 실행해 결과를 모으는 대신 코드와 명세를 분석한다. 기본적으로 정수 오버플로와 패닉의 부재를 검사하며 도달하지 않아야 할 상태도 확인한다. 코드가 컴파일된다는 사실보다 더 구체적인 성질을 다루지만 지원하는 언어 기능과 검증 범위를 확인해야 한다.
안전성과 기능 정확성
패닉이 발생하지 않는 함수라도 잘못된 값을 반환할 수 있다. 계산 결과가 어떤 관계를 만족해야 하는지는 전제조건과 사후조건 등으로 기술한다. 반복문에는 유지되어야 할 성질을 명시할 수 있다. 외부 라이브러리의 동작을 어떻게 가정했는지도 검증 결과의 의미에 포함된다.
설정과 결과의 경계
오버플로 검사를 끄고 정수를 무한 범위로 취급하는 설정은 확인하는 모델 자체를 바꾼다. 따라서 설정이 다른 성공 결과를 같은 보증으로 받아들이지 않는다. IDE 확장이나 명령행 도구로 실행할 수 있지만 일반 Rust 빌드와 필요한 환경이 다를 수 있다. 명세와 도구 버전 및 검증 조건을 함께 유지하며 실패 원인을 조사한다.
관련 문서
Creusot / Kani / Miri / Loom 동시성 테스트