Разные части Топаза отвечают на разные вопросы. Смысл программы определяется языком, допустимость исходного файла проверяет инструментарий, а фактическое поведение подтверждают наблюдения в конкретной среде.
Какой источник отвечает на ваш вопрос?
| Источник | Что он устанавливает | Чего он не устанавливает |
|---|---|---|
| Спецификация языка (SPEC) | Канонический синтаксис, типы, семантику и наблюдаемые границы языка | Отсутствие ошибок в реализации или поддержку каждой возможности всеми целями |
| Средство статической проверки | Разбирается ли исходный код, разрешены ли имена и типы и допустима ли программа для выбранного применения | Поведение при выполнении, равенство результатов разных целей или правильность внешней программы |
| Интерпретатор и цели сборки | Непосредственное поведение или созданный продукт для цели; неподдерживаемое поведение отклоняется явно | Одинаковое внутреннее устройство, одинаковую производительность или всеобщую поддержку возможностей |
| Канонические примеры | Один поддерживаемый способ записи или рабочий процесс с наблюдаемым результатом | Исчерпывающее покрытие или допустимость синтаксиса, которого нет в спецификации |
| Тесты и отчёты о проверке | Наблюдения для указанных входных данных, инструментов, сред, профилей и ограничений | Формальную верификацию, полное равенство реализаций или отсутствие расхождений вне проведённой проверки |
Практический порядок проверки
- Выберите нужную форму в текущем справочнике языка и канонических примерах.
- Выполните
topaz check, чтобы найти ошибки синтаксиса, имён, типов и выбранного профиля. - Запустите программу и тесты. Зафиксируйте важные вывод, диагностику, изменения файлов и код завершения.
- Соберите нужную цель и проверьте её документированные ограничения. Цель должна явно завершиться ошибкой, если не может сохранить требуемое поведение.
- Читая результат теста или отчёт о проверке, учитывайте точные входные данные, среду и пределы проверки.
Обычная последовательность команд:
topaz check main.tpz
topaz run main.tpz
topaz build main.tpz --out-dir build
Сравнение свидетельств компилятора
Канонические наблюдения позволяют сравнивать именованные границы двух запусков,
не расширяя утверждение дальше выбранных свидетельств. semantic сравнивает
по порядку набор исходников, этапы компилятора, диагностику и исход;
generated-source — точный созданный код Rust; provenance — идентичность
производителя; native-binary — точные байты исполняемых файлов для одной
цели. Равенство одного слоя не означает равенства другого, а успешный прогон
рабочей нагрузки является ограниченным свидетельством, но не доказательством
эквивалентности всего языка.