18검증 문제

ready condition으로 method 제한하기

1. 문제와 수정 범위

bump는 카운터가 3 미만인 동안에만 상태를 바꿀 수 있어야 합니다. Starter에는 method ready condition이 없으므로 drive가 다섯 번의 시도에서 모두 실행됩니다. 공개 실행의 최종 카운터가 5가 되는 원인은 호출자 guard가 아니라 제한 없는 method 계약입니다.

수정 위치는 bump method header입니다. 카운터 초기값과 폭, method body, drive, advance는 그대로 두세요. 호출자 한 곳에 조건을 복사하지 말고, 모든 호출자에게 적용되는 method 계약을 만드세요.

2. Starter 읽기와 실행 예측

선언은 다음 순서로 확인해 보세요.

순서	선언	확인할 계약
1	`BoundedCounter`	상태를 바꾸는 method와 값을 읽는 method
2	`count`와 `bump`	갱신 대상과 한 번 호출할 때의 증가량
3	`drive`	method 호출을 시도하는 사이클 범위
4	`advance`	method 실행 여부와 독립적으로 진행하는 관찰 사이클
5	`show`	다섯 관찰 사이클 뒤 표시하는 값

수정하기 전에는 cycles < 5인 동안 drive와 advance가 함께 실행될 수 있습니다. bump가 항상 ready이므로 카운터는 시도할 때마다 증가합니다. 수정한 뒤에는 advance가 계속 진행하지만, count가 한계에 도달하면 drive action 전체가 비활성화되어야 합니다.

3. 최소 수정과 완료 조건

Method ready condition은 해당 method를 호출하는 모든 rule의 합성 조건에 포함됩니다. 현재 상태와 상한을 비교하는 조건을 method header에 추가하세요. 한 단계 증가시키는 body와 호출 횟수를 만드는 mkTop은 이미 올바릅니다.

여러 사이클의 상태는 다음 계약을 만족해야 합니다.

진입 시점의 `count`	`bump` ready	호출자 전이 뒤 상태
0	참	1
1	참	2
2	참	3
3	거짓	3
3	거짓	3

카운터는 0에서 시작해 세 번만 증가하고, 이후 시도에서도 3을 유지해야 합니다. 한 번 표시된 값만 3으로 맞추거나 drive에만 조건을 두면 method를 호출하는 다른 rule을 보호하지 못하므로 완료가 아닙니다.

4. 단계형 힌트

힌트 1 — 계약의 소유자

count를 바꾸는 모든 호출을 제한해야 합니다. 호출자 한 곳이 아니라 상태 변경 연산을 정의한 선언에 조건을 두세요.

힌트 2 — 문법 위치

수정 지점은 bump의 빈 인자 목록과 method header의 세미콜론 사이입니다. Method body는 바꾸지 않습니다.

힌트 3 — 경계 조건

현재 값이 2일 때는 호출을 허용하고 3일 때는 허용하지 않는 비교식을 쓰세요. 상한은 포함하지 않습니다.

5. 추가 실험

필수 수정을 확인한 뒤 method의 상한만 4로 바꿔 보세요. 실행 전에 최종 카운터와 성공하는 호출 수를 예측해 보세요. advance는 여전히 다섯 관찰 사이클을 끝내고, drive만 한 번 더 실행되어야 합니다. 이 실험은 채점 조건이 아닙니다.