Корректность компилятора
-
Основы корректности компилятора
- Корректность компилятора — раздел компьютерных наук, проверяющий соответствие компилятора спецификации языка.
- Методы включают разработку с использованием формальных методов и тестирование (валидацию) существующих компиляторов.
-
Формальная проверка компилятора
- Два основных подхода: проверка корректности для всех входных данных и проверка корректности перевода конкретной программы.
- Валидация формальными методами включает длинную цепочку дедуктивной логики, но может содержать ошибки из-за сложности инструмента поиска доказательств.
- CompCert и CakeML — примеры формально проверенных оптимизирующих компиляторов.
- Семантически ориентированная генерация компилятора — другой подход к получению формально корректного компилятора.
-
Проверка перевода
- Проверка перевода направлена на автоматическое доказательство корректности компиляции данной программы.
- Проверка перевода может использовать существующую реализацию компилятора и гарантировать корректность для всех входных данных.
-
Тестирование компилятора
- Тестирование является важной частью разработки компилятора, но часто игнорируется в литературе.
- Регрессионное тестирование и тестирование вызовов процедур описаны в литературе.
- Многие выпущенные компиляторы содержат ошибки в корректности кода.
- Фаззинг и сокращение тестового примера — распространенные методы тестирования компиляторов.