Войти
В вычислениях, корректность компилятора - это раздел информатики, который занимается попытками чтобы показать, что компилятор ведет себя в соответствии со своей спецификацией языка . Методы включают разработку компилятора с использованием формальных методов и использование строгого тестирования (часто называемого проверкой компилятора) на существующем компиляторе.
Два основных формальной верификации подхода для установления правильности компиляции - это подтверждение корректности компилятора для всех входных данных и подтверждение правильности компиляции конкретной программы (проверка перевода).
Проверка компилятора формальными методами включает длинную цепочку формальной, дедуктивной логики. Однако, поскольку инструмент для поиска доказательства (средство доказательства теорем ) реализован программно и является сложным, высока вероятность, что он будет содержать ошибки. Один из подходов заключался в использовании инструмента, который проверяет доказательство (средство проверки доказательства ), которое, поскольку оно намного проще, чем средство поиска корректуры, с меньшей вероятностью будет содержать ошибки.
Ярким примером этого подхода является CompCert, который является официально проверенным оптимизирующим компилятором большого подмножества C99.
Другой проверенный компилятор был разработан в проекте CakeML, который устанавливает правильность существенного подмножества языка программирования Standard ML с помощью HOL (помощник по проверке).
Другой подход к получению формально корректного компилятора - использование генерации компилятора, ориентированной на семантику.
В отличие от попытки доказать, что компилятор корректен для всех допустимых программ ввода, проверка перевода направлена на автоматическое установление того, что данная программа ввода скомпилирована правильно. Доказательство правильной компиляции данной программы потенциально проще, чем доказательство правильности компилятора для всех программ, но все же требует символических рассуждений, потому что фиксированная программа может по-прежнему работать с произвольно большими входными данными и выполняться в течение сколь угодно долгого времени. Проверка перевода может повторно использовать существующую реализацию компилятора, создавая для данной компиляции доказательство того, что компиляция была правильной. Проверка перевода может использоваться даже с компилятором, который иногда генерирует неправильный код, если этот неправильный код не проявляется для данной программы. В зависимости от входной программы проверка перевода может завершиться ошибкой (из-за того, что сгенерированный код неверен или метод проверки перевода слишком слаб, чтобы показать правильность). Однако, если проверка перевода прошла успешно, программа компилятора гарантированно верна для всех входных данных.
Тестирование представляет собой значительную часть усилий по доставке компилятора, но сравнительно мало освещается в стандартной литературе. В издании Aho, Sethi, Ullman 1986 г. есть одностраничный раздел о тестировании компилятора без именованных примеров. В издании 2006 года отсутствует раздел о тестировании, но подчеркивается его важность: «Оптимизация компиляторов настолько сложна, что мы осмеливаемся сказать, что ни один оптимизирующий компилятор не является полностью безошибочным! Таким образом, самая важная цель при написании компилятора - сделать его правильным ». Fraser Hanson 1995 имеет краткий раздел о регрессионном тестировании ; исходный код доступен. Bailey Davidson 2003 охватывает тестирование вызовов процедур. Ряд статей подтверждают, что многие выпущенные компиляторы содержат значительные ошибки корректности кода. Sheridan 2007, вероятно, самая последняя статья в журнале по общему тестированию компиляторов. Для большинства целей наибольший объем доступной информации о тестировании компилятора - это наборы проверки Fortran и Cobol.
Другими распространенными методами при тестировании компиляторов являются фаззинг (который генерирует случайные программы для поиска ошибок в компиляторе) и сокращение тестового примера (которое пытается минимизировать нашел тестовый пример, чтобы облегчить понимание).
