결함 재발 검출 증명

통과만으로 검출 능력이 보이지 않습니다

회귀 검사는 수정된 코드에서 통과하는 것만으로 충분히 설명되지 않습니다. 원래 결함을 넣어도 통과한다면 그 검사는 해당 결함을 잡지 못합니다. 같은 입력과 기대값으로 알려진 결함 버전과 수정 버전을 비교하면 검사에 검출 능력이 있는지 확인할 수 있습니다. 이번에는 m09의 지연·공유 상태 모형을 그대로 사용합니다. 실제 회원 앱의 결함을 고쳤다는 주장은 하지 않고 가상 모형의 재발 검출을 증명합니다.

결함 버전은 baseline 정책입니다. 한 tick만 기다리고 write와 read가 shared key를 공유합니다. 수정 버전은 repair 정책으로 준비 상태와 새이름을 제한된 budget까지 관찰하고 실행·검사별 key를 사용합니다. 두 버전에 동일한 seed 0~9를 넣습니다. seed가 지연과 순서를 결정하므로 매번 다른 입력으로 비교하는 문제가 없습니다. 가상 시계가 다루지 않는 실제 네트워크나 DOM 대기는 여전히 별도 검증이 필요합니다.

이 레슨의 local 실습은 qa-regression-proof입니다. 제공 engine.cjs와 repair.cjs는 앞 미션 solution에서 가져온 코드입니다. 학습자는 oracle.cjs라는 판정 함수만 완성합니다. 모형 자체가 성공을 반환해도 failure 필드가 NONE이 아니면 거절해야 합니다. 성공 플래그와 실패 코드의 모순을 확인하는 것은 검사기 신뢰성의 작은 경계 사례입니다. 기대값을 관찰값에 맞춰 느슨하게 바꾸는 방법으로 통과시키지 않습니다.

동일 검사를 두 버전에 적용합니다

proof.cjs는 observe로 얻은 관찰을 같은 oracle에 넣습니다. baseline의 예상 실패 배열은 STATE_LEAK·NONE·SAVE_NOT_READY 등으로 고정돼 있습니다. 수정 버전은 모든 seed에서 성공해야 합니다. seed 1·5·9에서는 결함 버전도 통과하므로 결함이 있다고 모든 입력이 실패해야 한다고 기대하지 않습니다. 입력 조건과 실패 양상을 연결해야 재현 보고서에서 왜 특정 입력을 골랐는지 설명할 수 있습니다.

검사 대상의 실패와 비교 도구의 실패를 구분합니다. baseline에서 7건을 검출하고 repair에서 10건이 통과하면 proof.cjs는 종료 코드 0으로 끝납니다. 이는 결함 버전이 정상이라는 뜻이 아니라 예상한 실패를 검출했다는 뜻입니다. oracle이 결함 관찰을 놓치거나 repair 관찰을 잘못 거절하면 ORACLE_MISMATCH를 던집니다. 알려진 실패를 합의된 기대 결과로 비교하는 도구의 실행과 앱 테스트 결과를 같은 열에 넣지 않습니다.

각 행에는 seed, buggy의 pass·failure, fixed의 pass·failure를 남깁니다. 보고서에 재시도 0을 넣는 이유는 실패한 뒤 통과한 결과만 선택하는 오해를 막기 위해서입니다. 이전 기록은 그대로 보존하고 이번 보고서는 quality/proof 아래에 생성합니다. 한 실행에서 얻은 관찰이 무엇인지 분명히 하며, seed가 열 개라는 이유로 실환경의 모든 지연과 실행 순서를 확인했다고 해석하지 않습니다.

독립적인 기대값을 지킵니다

oracle의 정상 조건은 관찰 객체가 있고 pass가 불리언 true이며 failure가 문자열 NONE인 경우입니다. null이나 빈 객체는 실패로 처리합니다. pass가 문자열 true인 값도 성공으로 받지 않습니다. 실제 앱에 연결할 검사에서도 타입과 의미를 구분하는 습관이 필요합니다. 성공 여부를 JavaScript의 truthy 판정에만 맡기면 문자열과 누락 필드를 예상과 다르게 처리할 수 있습니다.

starter는 pass만 확인하므로 seed 비교 일부는 이미 통과합니다. 하지만 pass=true, failure=STATE_LEAK라는 모순 입력을 넣으면 ORACLE_BOUNDARY로 실패합니다. 이것은 런타임 설치 문제나 앱 서버 접속 문제가 아니라 검사 조건 부족입니다. 모범 답안은 pass와 failure를 동시에 비교합니다. 원래 요구와 관계없는 조건을 추가해 우연히 실패하게 만드는 방식은 검출 증명이 아니므로 어떤 계약을 검사했는지 설명합니다.

기대 실패 코드는 모형의 규칙에서 정합니다. baseline의 실제 출력 배열을 그대로 기대값으로 복사하면 나중에 결함 코드가 달라져도 알아차리지 못할 수 있습니다. 이번 배열은 seed별 지연과 write/read 순서를 읽고 검토하는 교육용 계약입니다. 상태 누수가 일어나는 순서와 준비가 늦어지는 지연을 따로 설명합니다. 팀에서는 관찰 자료와 독립된 합의 기준을 리뷰한 뒤 자동 검사에 고정합니다.

명령과 증거를 함께 보존합니다

압축을 푼 루트에서 bash check.sh를 실행하면 proof.cjs가 보고서를 씁니다. 결과는 buggy 3/10 PASS, fixed 10/10 PASS와 retries=0입니다. reports/proof.json은 모형·수정 정책·판정 코드의 SHA-256과 행별 관찰을 포함합니다. 해시는 어떤 바이트를 사용했는지 식별하는 장치입니다. 해시가 같다고 기능이 옳다는 증거가 생기는 것은 아니며, 경로와 실행 명령·범위가 같이 있어야 비교할 수 있습니다.

환경 오류는 의미 있는 검출 실패와 다르게 읽습니다. node command not found라면 Node 실행 파일을 준비해야 하며 이를 결함 검출 성공으로 세지 않습니다. Cannot find module은 압축 루트나 파일 구성을 확인할 신호입니다. ORACLE_MISMATCH seed=2처럼 출력되면 seed 2의 지연과 expectedFailures를 대조합니다. ORACLE_BOUNDARY가 나오면 null·모순 필드 검사부터 확인하고 engine을 수정해 오류를 숨기지 않습니다.

본문에 성공 출력이 있다고 starter에서도 처음부터 성공해야 하는 것은 아닙니다. 따라하기는 solution 실행에서 얻은 결과를 비교 기준으로 제시합니다. starter에서 실패를 읽고 oracle을 완성한 후 동일 명령으로 다시 확인합니다. 학습자가 보고서를 열었을 때 모든 fixed 행이 통과하며 buggy의 실패가 지워지지 않았는지 확인합니다. 실행마다 시간 수치는 달라질 수 있으므로 비교에는 seed·결과·실패 코드와 대상 해시를 사용합니다.

실제 결함 보고서와 연결할 때 한계를 표시합니다

앞 프로젝트의 DEF-01과 DEF-02는 가입 경계와 공백 닉네임에 관한 이전 앱 결함입니다. 이번 가상 모형의 SAVE_NOT_READY와 STATE_LEAK는 그 결함 ID와 같은 문제가 아닙니다. 모형 통과를 근거로 두 결함을 해결 처리하지 않습니다. 최종 추적표에서는 과거 결함 자료의 경로를 연결하되 이번 대상 버전에서 재검증하지 않았다는 표시를 유지합니다. 실제 결함 회귀는 해당 입력과 저장 관찰을 같은 계약으로 재실행해야 합니다.

증거 리뷰에서는 알려진 결함이 들어간 버전의 실패, 수정 버전의 성공, 두 실행에 쓰인 같은 검사, 남은 한계를 순서대로 설명합니다. 누군가 수정 코드만 보고 통과했다고 말하면 결함 버전의 행을 먼저 요청합니다. 누군가 모든 기능을 자동화했다고 말하면 모형과 실제 앱의 경계를 묻습니다. 검출 증명은 테스트 숫자를 늘리는 일이 아니라, 어떤 오류를 어떤 입력으로 실제 구분했는지 보여 주는 작업입니다.