타입과 계약의 역할
타입 표기는 입력을 어떤 종류의 값으로 다룰지 알려 주고, 계약은 함수가 지켜야 하는 조건을 표현한다. CrossHair는 함수를 기호값으로 반복 호출하며 조건을 깨는 실행을 찾는다. 타입 검사가 통과하는 것과 계약을 만족하는지는 다른 질문이다.
경로 조건을 이용한 탐색
실행 중 분기가 생기면 입력이 그 경로에 들어갈 조건을 논리적으로 다룬다. 내장 타입과 사용자 정의 클래스, 표준 라이브러리 일부를 위한 기호 추론을 제공한다. 지원되지 않는 동작이 있으면 분석 범위에 영향을 줄 수 있다.
계약 검사 이외의 활용
함수의 실행 경로를 이용해 단위 테스트를 생성하거나 두 함수의 행동 차이를 찾는 기능도 있다. 차이를 찾는 작업은 어느 구현이 요구 사항에 맞는지 자동으로 정하는 것과 다르다. 반례는 실제 입력으로 재현하고 계약 자체도 함께 검토한다.
관련 문서
Nagini / Atheris / Deal 계약 라이브러리 / Pynguin