자원과 함수 계약
전제조건과 사후조건으로 함수가 사용할 자원과 보장할 결과를 기술한다. 분리 논리는 메모리 영역과 접근 권한을 구분하는 명세에 활용된다. 단일 스레드뿐 아니라 여러 스레드가 자원을 공유하는 코드도 다룬다. 어떤 공유 규칙을 가정하고 확인하는지는 명세에 분명히 나타나야 한다.
보조 정의와 증명 함수
귀납적 자료형과 순수 함수 및 추상 술어로 복잡한 명세를 구성할 수 있다. 보조 정리를 함수 형태로 작성해 필요한 논리 관계를 설명하며 이런 함수의 종료와 부수 효과가 없는지도 확인한다. 증명 코드가 많거나 검증이 빠르다는 사실만으로 명세가 요구사항을 충분히 다룬다고 볼 수는 없다.
사례의 범위와 도입
IDE와 명령행 및 편집기 확장을 통해 사용할 수 있다. 특정 자료 구조나 동시 알고리즘의 검증 사례가 있어도 해당 언어의 모든 기능과 모든 라이브러리를 자동 검증한다는 뜻은 아니다. 부분 증명과 단순화한 구현의 증명을 구분한다. 대상 기능의 지원 범위와 계약의 가정 및 확인하지 않은 부분을 함께 관리한다.