토파즈를 이루는 각 요소는 서로 다른 질문에 답합니다. 프로그램의 의미는 언어 정의를 기준으로 판단합니다. 소스를 받아들일 수 있는지는 검사기로 확인합니다. 실제 동작은 지정한 환경에서 얻은 실행 결과로 판단해야 합니다.
무엇을 기준으로 판단해야 하나요?
| 기준 | 확인할 수 있는 것 | 확인할 수 없는 것 |
|---|---|---|
| 언어 명세(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를 씁니다. 한 계층이 일치해도 다른 계층까지 일치한다는 뜻은
아닙니다. 워크로드 통과는 범위가 정해진 증거이지 전체 언어 동등성의 증명은
아닙니다.