12장. Property와 model-based test로 상태 공간을 넓힌다

금액은 음수가 아니고, 취소된 예약은 다시 확정되지 않으며, 같은 command sequence의 재실행은 결과가 같다는 성질을 정의한다. generator가 다양한 순서와 경계값을 만들고 실패 입력을 줄여 최소 반례를 남긴다.

상태 머신 모델에 open -> held -> confirmed -> completed|cancelled 전이를 두고 허용되지 않은 명령을 생성한다. 예제 test를 대체하지 않고 사람이 놓치기 쉬운 조합을 찾는 데 사용한다. seed를 저장해 CI 실패를 로컬에서 다시 실행한다.