한 번의 호출보다 상태 변화
계약의 오류는 함수 하나보다 여러 호출이 이어질 때 나타날 수 있다. Echidna는 호출 순서를 생성하고 계약 상태가 바뀌는 동안 속성을 확인한다. 실패가 발견되면 해당 조건을 깨는 시퀀스를 분석할 수 있다.
검사할 성질을 작성하기
기본 속성 모드에서는 정해진 형태의 불리언 반환 함수로 유지되어야 할 조건을 표현한다. 단언문 검사 등 다른 테스트 모드도 있다. 실행 모드마다 무엇을 실패로 판단하는지가 다르므로 작성한 테스트의 형태와 설정을 맞춘다.
결과를 좁혀 이해하기
커버리지 유도 탐색과 입력 모음, 자동 최소화 기능은 실패 원인 분석에 도움을 준다. 그러나 퍼징 캠페인에서 반례가 없었다는 결과는 모든 상태의 안전성을 뜻하지 않는다. 초기 상태와 호출 가능한 함수, 사용한 모드를 함께 기록한다.