44검증 문제

잘못된 always-ready 계약 고치기

1. 문제와 수정 범위

크기가 정해진 큐에 값을 넣는 method의 Ready는 큐 상태에 따라 바뀌어야 합니다. BufferedSink.put은 깊이 1인 FIFOF의 enq를 호출하지만, 인터페이스는 put이 항상 준비되어 있다고 선언합니다. 가득 찬 큐에는 값을 넣을 수 없으므로 이 모순은 시뮬레이션 전, 컴파일 단계에서 검출됩니다.

인터페이스의 계약 선언만 수정하세요. FIFOF와 그 깊이, put과 take의 구현, mkTop은 그대로 둡니다.

2. starter 읽기와 컴파일 결과 예측

다음 순서로 계약을 따라가 보세요.

실행 전에 출력값보다 컴파일 결과를 먼저 예측해 보세요. 빈 큐에서는 enq가 준비되어 있지만, 가득 찬 큐에서는 준비되어 있지 않습니다. 모든 상태에서 참이어야 하는 선언을 증명할 수 없으므로 컴파일 오류가 발생합니다. 오류 메시지는 어트리뷰트를 가리키지만, 원인은 항목 하나로 가득 차는 큐 상태에 있습니다.

3. 최소 수정과 완료 조건

put의 실제 준비 조건이 생성되는 인터페이스에 드러나게 하세요. 잘못된 선언 한 곳만 고칩니다. 큐를 바꾸거나 늘리거나, 가득 찼는지 검사하는 조건을 직접 추가하거나, enq 본문을 다시 쓰지 마세요.

깊이를 늘려도 유한한 큐에는 가득 찬 상태가 있습니다. 준비 조건이 상수가 아니므로 Ready 핸드셰이크를 남기는 것이 정확한 계약입니다. 사실이 아닌 약속을 지워도 method의 기능은 줄지 않습니다. method 구현에 이미 있는 조건이 호출하는 쪽에 전달될 뿐입니다.

수정한 뒤 실행은 컴파일과 시뮬레이션을 마치고 buffered = 5a를 출력해야 합니다. 큐 용량은 항목 하나로 유지됩니다. 재사용되는 모듈 경계에서 put은 큐가 비어 있을 때 준비 상태이고, 항목이 차 있을 때는 준비 상태가 아니어야 합니다. 공개 입력 8'h5a만 맞추는 구현은 이 상태 계약을 만족하지 못합니다.

4. 단계형 힌트

5. 추가 실험

수정을 마친 뒤 큐 깊이가 2이고 take 없이 put을 연속 두 번 호출한다고 가정해 보세요. 호출이 받아들여질 때마다 항목 수가 어떻게 바뀌는지, Ready가 어느 사이클에 거짓이 되는지 예측해 보세요. 채점 대상이 아니므로 깊이를 바꿨다면 제출하기 전에 되돌리세요.