무작위 값 대신 기호값
기호 입력은 임의의 숫자 하나가 아니라 타입 범위와 제약을 만족하는 값들을 표현한다. 테스트는 입력 조건을 설정하고 계약을 호출한 뒤 결과를 단언하는 구조다. 가정이 너무 강하면 확인해야 할 입력을 제외할 수 있다.
초기 상태도 분석의 일부
테스트 준비 단계에서 계약을 생성하고 상태를 초기화한다. 생성자 인자도 기호값으로 구성할 수 있다. 같은 테스트라도 구체적인 초기 상태인지 기호적으로 설정한 상태인지에 따라 확인하는 경우의 범위가 달라진다.
실패 판정의 의미
단언문 위반을 찾는 것이 다른 모든 revert를 결함으로 보고하는 것과 같지는 않다. 호출 실패나 산술 오류를 확인하려면 그 행동을 관측하는 테스트를 따로 설계해야 한다. 배열 크기 등 기호화 제약과 지원 기능도 함께 확인한다.