정확성 오라클은(는) 무엇을 하나요?
약속된 동작을 반박할 수 있는 관찰을 선택하세요. 성공적인 검사가 무엇을 테스트하지 않은 채로 남겨두는지 명시하세요: 개수 비교, 구조 검사 및 의존성 증인은 서로 다른 속성을 관찰합니다 (NoREC 구현, SQLite 무결성 검사, Elle §4.3).
실제 경계에서 검사 도출하기
대상의 활성 구성, 공개 생성자(public producer) 및 지배 계약(governing contract)을 읽으세요. 합법적인 시작 상태, 연산 사전 조건, 허용된 오류 및 약속된 경계(하나의 연산, 명령문, 트랜잭션, 복구 또는 관찰된 히스토리)를 식별하세요. SQLite에서 ABORT는 하나의 명령문을 취소하는 반면, 지연된 외래 키(deferred foreign key)는 "트랜잭션이 COMMIT을 시도할 때까지 검사되지 않습니다" (SQLite ABORT, 지연된 외래 키). 가능하면 유효 설정을 쿼리하세요; 예를 들어 SQLite의 외래 키 설정은 "트랜잭션 내에서 no-op입니다" (SQLite foreign_keys).
탐색 범위를 확장하기 전에 구체적인 후보 관찰을 작성하세요:
- 약속: 정확히 금지된 결과 또는 효과와 그 계약 인용.
- 관찰: 위반을 허용된 동작과 구별하는 실제 반환 내용, 상태 또는 증인.
- 사전 조건 및 사각지대: 지원되는 구성, 유효한 상태, 생략된 정보 및 구별 불가능한 실행.
- 재현 증거: 입력 및 초기 상태, 연산 순서, 유효 구성 및 원시 관찰.
이는 간결한 설계 규칙이지 필수 스키마가 아닙니다. 그 목적은 제안된 검사에서 손실된 정보를 드러내는 것입니다; Elle의 관찰 모델은 왜 숨겨진 의존성이 단순히 더 많은 히스토리를 생성함으로써 복구될 수 없는지 보여줍니다: 맹목적인 레지스터 쓰기는 "히스토리를 파괴합니다" (Elle §§3–4.3). 자세한 경계 예시는 계약 예제를 참조하세요.
JavaScript에서 프로세스 종료 코드, 테스트 러너 상태 또는 깨끗한 콘솔은 그러한 관찰입니다: 그 의미는 유효 모드, 설치된 리스너, 러너 구성 및 빌드에 따라 달라집니다. uncaughtException 핸들러가 설치된 경우 Node의 프로세스는 핸들러가 process.exitCode를 설정하지 않는 한 "0으로 종료됩니다" (Node process, uncaughtException). Node, 테스트 러너, React 및 Playwright 채널에 대해서는 JavaScript 관찰 채널을 참조하세요.
관찰을 의심스러운 동작과 독립적으로 유지하기
예상 값이나 불변식(invariant)이 어떻게 얻어지는지 추적하세요. 대상과 검사기가 동일한 잘못된 답에 동의할 수 있게 하는 공유 코드와 가정을 식별하세요. 복사된 프로덕션 알고리즘보다는 정당화된 추상 모델, 독립적으로 명시된 불변식 또는 유효한 관계를 선호하세요. 두 번째 구현은 하나의 옵션입니다: SQLite의 SQL Logic Test는 여러 엔진에 대해 명령문을 실행하고 "모두 동일한 답변을 얻는지 확인합니다". 동일 엔진 관계도 또 다른 옵션입니다: SQLite는 최적화가 비활성화된 상태에서 스위트를 재실행하고, SQLancer의 NoREC는 최적화된 쿼리를 최적화되지 않은 쿼리와 비교합니다 (SQLite 테스트 §2, §9, NoREC 구현).
실제로 비교되는 정보를 측정하세요. 동일한 행 개수가 행의 동일성을 확립하지는 않습니다; 정상적인 integrity_check는 참조 무결성을 확립하지 않는데, 이는 "FOREIGN KEY 오류를 찾지 않기" 때문입니다. 유효한 부분 검사를 보존하고 대상 보장이 요구하는 경우에만 보완적인 관찰을 추가하세요 (NoREC 구현, SQLite 무결성 검사). 참조, 정규화 또는 증인을 선택할 때는 부분 관찰을 참조하세요.
허용된 오류와 그 효과 확인하기
허용된 사후 상태를 반환된 상태와 별도로 도출하세요. SQLite의 ABORT와 FAIL은 모두 제약 조건 오류를 반환하지만, ABORT는 실패한 명령문을 취소하는 반면 FAIL은 "실패한 SQL 명령문의 이전 변경 사항을 취소하지 않습니다". 오류 전용 단정은 잘못된 효과를 놓칠 수 있습니다; 포괄적인 롤백 단정은 합법적인 동작을 거부할 수 있습니다 (SQLite 충돌 정책).
유효한 사전 조건을 가진 실제 약속에 대한 관찰자를 선택하세요. SQLite 참조 검사의 경우, 적용 가능한 외래 키 관찰, 유효한 시행 설정 및 합법적인 NULL 의미론을 사용하세요; 일반적인 무결성 결과를 대체하지 마세요 (SQLite 외래 키, foreign_key_check). 이는 임의의 API에 대한 기본값이 아니라 실제로 작동하는 계약입니다.
검사의 결과와 한계 보존하기
그 차이가 결론에 영향을 미칠 때마다 평가된 속성과 거부된 입력, 예상된 오류, 건너뛴 검사 및 불충분한 관찰을 구분하세요. NoREC는 예상 쿼리 오류 후와 같은 경우에 개수가 -1 센티넬일 때 이를 동등성으로 간주하지 않고 비교를 건너뛰며, 예상치 못한 오류를 실패로 보고합니다. Elle의 완전성은 기록된 정보에 의존하며, "관찰은 거의 완전하지 않습니다" (NoREC 구현, Elle §4.3).
harness-sensitivity를 사용하여 관찰이 대표적인 독립적으로 정당화된 위반에 도달하고 이를 거부함을 확립하세요. evidence-based-triage를 위해 원시 증인을 보관하세요: Elle 자체 문서에서는 레이블을 최종 권위로 취급하지 말고 "보고된 이상 징후를 수동으로 확인"할 것을 권장합니다 (Elle README). 일반적인 탐색 할당은 bugfinding-campaign에 속합니다.
선택된 전문 추론을 semantic-differential-testing, metamorphic-testing, linearizability-checking, transactional-history-testing, numerical-oracles, resource-complexity-testing 또는 liveness-testing으로 라우팅하세요; 이 스킬은 계약에서 관찰로의 결정을 소유합니다. 오해를 불러일으키는 지름길에 대해서는 일반적인 실수를 참조하세요.
사용 가능한 오라클 반환하기
생성자, 인용된 보장, 유효한 사전 조건, 실행 가능한 관찰 및 결과 해석과 함께 작동하는 허용/금지 구분을 반환하세요. 무엇이 관찰 불가능한 상태로 남아 있고 어떤 증거가 재play에서 살아남아야 하는지 명시하세요. 입증된 모순은 실제로 검사된 보장과 가정만을 지원합니다 (Elle §§4.3 and 9).