타입보다 구체적인 계약
일반 타입이 값의 종류를 나타낸다면 refinement는 그 값이 만족할 논리 조건을 더한다. 비어 있지 않은 목록이나 같은 길이의 자료처럼 함수가 요구하는 입력 관계를 표현할 수 있다. 조건은 호출하는 쪽에도 전달되므로 자료를 사용하는 지점에서 필요한 계약을 확인한다.
종료와 기능 정확성
재귀 함수의 종료를 위한 척도와 결과가 만족할 성질을 명세할 수 있다. 등식적 증명을 Haskell 함수 형태로 작성하는 흐름도 제공한다. 명세가 약하면 요구한 결과를 충분히 확인하지 못하고 가정이 과하면 실제 사용 상황이 범위에서 빠질 수 있다. 일반 타입 검사와 추가 논리 조건의 역할을 구분한다.
컴파일 환경과 결과 관리
GHC 플러그인과 SMT solver 등 필요한 구성을 갖추어 실행한다. 프로젝트는 특정 GHC 버전에 맞춰 지원하는 정책을 설명하므로 임의의 컴파일러와 조합할 수 있다고 가정하지 않는다. 설치한 도구와 의존성이 달라지면 결과도 달라질 수 있다. 계약과 소스 및 실행 환경을 함께 유지하고 현재 변경이 다시 검증되었는지 확인한다.
관련 문서
Flux Rust 검증기 / Dafny / Creusot / Kani