Когда это нужно
Этот контракт нужен для сравнения, повторного запуска или аудита. Одного «того же входа» недостаточно, пока не указаны байты исходного кода, идентификатор исполнителя, профиль ресурсов и наблюдаемые каналы. Профиль ресурсов представляет собой именованный набор ограничений, в рамках которых выполняется запуск и о которых он отчитывается.
Разбор примера
Детерминированный запуск не гарантирует завершения любой программы. У каждого из существующих способов запуска Лиспекс есть именованные ограничения на вход, выход, переходы и управление, но они не учитывают каждый обход, операцию с точными числами, выделение, рендеринг и диагностику. Поэтому враждебный бесконечный цикл или программа с интенсивными выделениями может выйти за семантический охват текущего профиля. Время по часам остаётся эксплуатационным наблюдением, а не семантическим значением программы.
Как рассуждать
- Наблюдаемые каналы включают байты stdout, байты диагностики, статус выхода, порядок предупреждений, отчёт о ресурсах, представление итогового значения и при необходимости идентичность артефакта либо происхождения.
- Native и WebAssembly могут иметь разные закреплённые ограничения и при этом корректно сообщать результаты по ресурсам для своего профиля.
- Повторный запуск фиксирует исходный код, идентификатор исполнителя, ограничения и состав учитываемых наблюдений ещё до сравнения байтов.
Быстрый выбор
| Что закрепить до сравнения | Зачем | Пример наблюдения |
|---|---|---|
| байты исходного кода и входных данных | нормализация текста меняет идентичность | байты значения или диагностики |
| исполнитель и профиль | явно названы ограничения и охваченная часть языка | статус выхода и отчёт о ресурсах |
| состав наблюдений | детали среды вне наблюдений не входят в утверждение | stdout и порядок предупреждений |
| корпус и базовая линия | результат не должен выбирать набор проверки | совпадение, расхождение, несравнимость |
| идентичность артефакта при необходимости | свидетельство называет проверенный объект | квитанция или короткий отпечаток байтов движка |
Частая ошибка
Один лишь тайм-аут по настенным часам не является семантическим отчётом о ресурсах.
Текущие границы
- Совпадение на одном закреплённом наборе сравнений не является эквивалентностью всего языка или доказательством отсутствия расхождений.
- Прямое выполнение исходного кода встроенным интерпретатором и выполнение через виртуальную машину, исполняющую заранее подготовленные инструкции, одинаково предполагают доверенный исходный код правила. Ни то ни другое не рассчитано на сдерживание враждебного исходного кода, и ни там ни там нет детерминированных счётчиков всей работы и всех логических выделений.
- Тайм-аут, принудительно завершённый рабочий процесс, нехватка памяти у хоста, паника или ловушка означают эксплуатационное прерывание либо отказ движка. Они не дают ни решения, ни квитанции, которую можно передать дальше.
Куда дальше
Справочник сред выполнения показывает каждого исполнителя и его происхождение, а справочник проверенных поверхностей показывает точный охват поддерживаемых сравнений.