토파즈를 이루는 각 요소는 서로 다른 질문에 답합니다. 프로그램의 의미는 언어 정의를 기준으로 판단하고, 소스를 받아들일 수 있는지는 검사기로 확인하며, 실제 동작은 지정한 환경에서 얻은 실행 결과로 판단해야 합니다.
무엇을 기준으로 판단해야 하나요?
| 기준 | 확인할 수 있는 것 | 확인할 수 없는 것 |
|---|---|---|
| 언어 명세(SPEC) | 정본 문법, 타입, 의미 규칙과 관찰 가능한 언어 경계 | 구현에 결함이 없다는 보장이나 모든 출력 대상의 모든 기능 지원 |
| 검사기 | 이 소스의 구문·이름·타입이 올바르고 선택한 용도에서 허용되는지 | 실행 결과, 출력 대상 사이의 동등성이나 외부 프로그램의 정확성 |
| 해석기와 출력 대상 | 직접 실행 동작 또는 선택한 대상용 생성 제품. 보존할 수 없는 동작은 명확히 거부함 | 생성물 내부 구조와 성능이 같다는 보장이나 모든 대상의 보편적인 기능 지원 |
| 정본 예제 | 지원되는 한 가지 문법 형태나 작업 흐름과 관찰 가능한 결과 | 전체 언어를 빠짐없이 다룬다는 보장이나 명세에 없는 문법의 허용 |
| 테스트와 검증 기록 | 지정한 입력·도구·환경·프로필·한계에서 실제로 관찰한 결과 | 형식 검증, 언어 전체의 완전한 동등성이나 기록 밖에서 차이가 없다는 증명 |
실제 검증 순서
- 현재 언어 문서와 정본 예제에서 필요한 형식을 고릅니다.
topaz check로 구문·이름·타입과 선택한 프로필의 오류를 찾습니다.- 프로그램과 테스트를 실행하고 중요한 출력, 진단, 파일 변화와 종료 상태를 기록합니다.
- 사용할 출력 대상을 빌드하고 문서화된 제한을 확인합니다. 필요한 동작을 보존할 수 없는 대상은 명확히 실패해야 합니다.
- 테스트 결과나 검증 기록을 인용할 때는 입력, 실행 환경과 한계를 함께 확인합니다.
기본 명령 순서는 다음과 같습니다.
BASH
topaz check main.tpz
topaz run main.tpz
topaz build main.tpz --out-dir build
컴파일러 증거 비교
정규 컴파일러 관찰 자료를 사용하면 선택한 증거가 말해 주는 범위를 넘어서
주장하지 않고 두 실행의 이름 붙은 경계를 비교할 수 있습니다. 소스 집합부터
진단과 결과 상태까지 순서대로 비교하려면 semantic, 생성된 Rust 소스를
정확히 비교하려면 generated-source, 생성자 식별자를 비교하려면
provenance, 같은 대상을 위한 실행 파일 바이트를 비교하려면
native-binary를 사용합니다. 한 계층의 일치가 다른 계층의 일치를 뜻하지
않으며, 워크로드 통과는 범위가 정해진 증거이지 전체 언어 동등성의 증명은
아닙니다.