Корректность компилятора

• Основы корректности компилятора

  • Корректность компилятора – раздел компьютерных наук, проверяющий соответствие компилятора спецификации языка. 
  • Методы включают разработку с использованием формальных методов и тестирование (валидацию) существующих компиляторов. 

• Формальная проверка компилятора

  • Два основных подхода: проверка корректности для всех входных данных и проверка корректности перевода конкретной программы. 
  • Валидация формальными методами включает длинную цепочку дедуктивной логики, но может содержать ошибки из-за сложности инструмента поиска доказательств. 
  • CompCert и CakeML – примеры формально проверенных оптимизирующих компиляторов. 
  • Семантически ориентированная генерация компилятора – другой подход к получению формально корректного компилятора. 

• Проверка перевода

  • Проверка перевода направлена на автоматическое доказательство корректности компиляции данной программы. 
  • Проверка перевода может использовать существующую реализацию компилятора и гарантировать корректность для всех входных данных. 

• Тестирование компилятора

  • Тестирование является важной частью разработки компилятора, но часто игнорируется в литературе. 
  • Регрессионное тестирование и тестирование вызовов процедур описаны в литературе. 
  • Многие выпущенные компиляторы содержат ошибки в корректности кода. 
  • Фаззинг и сокращение тестового примера – распространенные методы тестирования компиляторов.