Различные компоненты Топаза отвечают за разные задачи. Смысл программы определяется языком, допустимость исходного файла проверяет инструментарий, а фактическое поведение подтверждают наблюдения в конкретной среде.
Какой источник отвечает на ваш вопрос?
| Источник | Что он устанавливает | Чего он не устанавливает |
|---|---|---|
Спецификация языка 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 — точные байты исполняемых файлов для одной
цели. Равенство одного слоя не означает равенства другого, а успешный прогон
рабочей нагрузки является ограниченным свидетельством, но не доказательством
эквивалентности всего языка.