Корректность компилятора
В вычислительной технике корректность компилятора — это раздел информатики, который пытается показать, что компилятор ведет себя в соответствии со спецификацией своего языка . [ нужна ссылка ] Методы включают разработку компилятора с использованием формальных методов и тщательное тестирование (часто называемое проверкой компилятора) существующего компилятора.
Формальная проверка [ править ]
![[икона]](http://upload.wikimedia.org/wikipedia/commons/thumb/1/1c/Wiki_letter_w_cropped.svg/20px-Wiki_letter_w_cropped.svg.png){kind=small} | Этот раздел нуждается в расширении . Вы можете помочь, добавив к нему . ( март 2009 г. ) |
Двумя основными подходами формальной проверки для установления правильности компиляции являются доказательство правильности компилятора для всех входных данных и доказательство правильности компиляции конкретной программы (проверка трансляции).
Корректность компилятора для всех программ ввода [ править ]
Проверка компилятора формальными методами включает в себя длинную цепочку формальной дедуктивной логики . [1] Однако, поскольку инструмент для поиска доказательства ( доказательство теорем ) реализован в программном обеспечении и является сложным, существует высокая вероятность того, что он будет содержать ошибки. Один из подходов заключался в использовании инструмента, проверяющего доказательство (средства проверки доказательств ), который, поскольку он намного проще, чем средство поиска доказательств, с меньшей вероятностью будет содержать ошибки.
Ярким примером такого подхода является CompCert , формально проверенный оптимизирующий компилятор большого подмножества C99 . [2] [3] [4]
Еще один проверенный компилятор был разработан в проекте CakeML: [5] который устанавливает корректность существенного подмножества Standard ML языка программирования с использованием HOL (помощник по проверке) .
Другой подход к получению формально правильного компилятора — использовать генерацию компилятора, управляемую семантикой. [6]
Проверка перевода: корректность компилятора в конкретной программе [ править ]
В отличие от попыток доказать, что компилятор корректен для всех допустимых входных программ, проверка перевода [7] Целью является автоматическое установление того, что данная входная программа скомпилирована правильно. Доказать правильную компиляцию данной программы потенциально проще, чем доказать правильность компилятора для всех программ, но все же требует символических рассуждений, поскольку фиксированная программа может по-прежнему работать с сколь угодно большими входными данными и работать сколь угодно долго. Проверка перевода может повторно использовать существующую реализацию компилятора, генерируя для данной компиляции доказательство того, что компиляция была правильной.Проверка перевода может использоваться даже с компилятором, который иногда генерирует неправильный код, пока эта некорректность не проявляется для данной программы. В зависимости от входной программы проверка перевода может завершиться неудачей (поскольку сгенерированный код неверен или метод проверки перевода слишком слаб, чтобы показать правильность). Однако если проверка перевода прошла успешно, то скомпилированная программа гарантированно будет корректной для всех входных данных.
Тестирование [ править ]
Тестирование представляет собой значительную часть усилий по выпуску компилятора, но ему сравнительно мало внимания уделяется в стандартной литературе. В издании Aho, Sethi & Ullman 1986 года есть одностраничный раздел, посвященный тестированию компилятора, без названных примеров. [8] В издании 2006 года отсутствует раздел о тестировании, но подчеркивается его важность: «Оптимизировать компиляторы настолько сложно, что мы осмеливаемся сказать, что ни один оптимизирующий компилятор не является полностью безошибочным! Таким образом, самая важная цель при написании компилятора — сделать его корректным». [9] В Fraser & Hanson 1995 есть краткий раздел, посвященный регрессионному тестированию ; исходный код доступен. [10] Bailey & Davidson, 2003 г., посвящено тестированию вызовов процедур. [11] Ряд статей подтверждает, что многие выпущенные компиляторы имеют серьезные ошибки в корректности кода. [12] Sheridan 2007 — вероятно, самая последняя журнальная статья по общему тестированию компиляторов. [13] В большинстве случаев самый большой объём информации, доступной по тестированию компилятора, — это Fortran. [14] и Кобол [15] комплекты валидации.
при тестировании компиляторов. Другие распространенные приемы фаззинга [16] (который генерирует случайные программы для поиска ошибок в компиляторе) и сокращение тестовых примеров (который пытается минимизировать найденный тестовый пример, чтобы облегчить его понимание). [17]
См. также [ править ]
- Компилятор
- Верификация и валидация (программное обеспечение)
- Корректность (информатика)
- Компилятор C CompCert — формально проверенный компилятор C.
- Размышления о доверии
Ссылки [ править ]
- ^ Де Милло, РА; Липтон, Р.Дж.; Перлис, Эй Джей (1979). «Социальные процессы и доказательства теорем и программ» . Коммуникации АКМ . 22 (5): 271–280. дои : 10.1145/359104.359106 . S2CID 6794058 .
- ^ Лерой, X. (2006). «Формальная сертификация серверной части компилятора или: программирование компилятора с помощью помощника по проверке». Уведомления ACM SIGPLAN . 41 : 42–54. дои : 10.1145/1111320.1111042 .
- ^ Лерой, Ксавье (1 декабря 2009 г.). «Формально проверенный серверный компонент компилятора». Журнал автоматизированного рассуждения . 43 (4): 363–446. arXiv : 0902.2137 . дои : 10.1007/s10817-009-9155-4 . ISSN 0168-7433 . S2CID 87730 .
- ^ «CompCert — компилятор CompCert C» . compcert.inria.fr . Проверено 21 июля 2017 г.
- ^ «CakeML: проверенная реализация машинного обучения» .
- ^ Стефан Диль, Генерация компиляторов и абстрактных машин , управляемая естественной семантикой, Формальные аспекты вычислений, Vol. 12 (2), Springer Verlag, 2000. дои : 10.1007/PL00003929
- ^ Пнуэли, Амир; Сигел, Майкл; Сингерман, Эли. Проверка перевода . Инструменты и алгоритмы построения и анализа систем, 4-я Международная конференция TACAS '98.
- ^ Составители: принципы, методы и инструменты , ниже 1986, стр. 731.
- ^ там же, 2006, с. 16.
- ^ Кристофер Фрейзер; Дэвид Хэнсон (1995). Переназначаемый компилятор C: проектирование и реализация . Бенджамин/Каммингс Паблишинг. ISBN 978-0-8053-1670-4 . , стр. 531–3.
- ^ Марк В. Бэйли; Джек В. Дэвидсон (2003). «Автоматическое обнаружение и диагностика ошибок в сгенерированном коде для вызовов процедур» (PDF) . Транзакции IEEE по разработке программного обеспечения . 29 (11): 1031–1042. CiteSeerX 10.1.1.15.4829 . дои : 10.1109/tse.2003.1245304 . Архивировано из оригинала (PDF) 28 апреля 2003 г. Проверено 24 марта 2009 г. , с. 1040.
- ^ Например, Кристиан Линдиг (2005). «Случайное тестирование соглашений о вызовах C» (PDF) . Материалы шестого международного семинара по автоматизированной отладке . АКМ. ISBN 1-59593-050-7 . Архивировано из оригинала (PDF) 11 июля 2011 г. Проверено 24 марта 2009 г. , и Эрик Эйде; Джон Регер (2008). «Волатильные данные неправильно составлены, и что с этим делать» (PDF) . Материалы 7-й международной конференции ACM по встраиваемому программному обеспечению . АКМ. ISBN 978-1-60558-468-3 . Проверено 24 марта 2009 г.
- ^ Флэш Шеридан (2007). «Практическое тестирование компилятора C99 с использованием сравнения выходных данных» (PDF) . Программное обеспечение: практика и опыт . 37 (14): 1475–1488. arXiv : 2202.07390 . дои : 10.1002/спе.812 . S2CID 9752084 . Проверено 24 марта 2009 г. Библиография на «Библиография по тестированию компиляторов» . Проверено 13 марта 2009 г. .
- ^ «Источник пакета проверки Фортрана» . Проверено 1 сентября 2011 г.
- ^ «Источник пакета проверки Cobol» . Проверено 1 сентября 2011 г.
- ^ Чен, Ян; Грос, Алекс; Чжан, Чаоцян; Вонг, Венг-Кин; Папоротник, Сяоли; Эйде, Эрик; Регер, Джон (2013). «Укрощение фаззеров компилятора». Материалы 34-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . ПЛДИ '13. Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 197–208. CiteSeerX 10.1.1.308.5541 . дои : 10.1145/2491956.2462173 . ISBN 9781450320146 . S2CID 207205614 .
- ^ Регер, Джон; Чен, Ян; Куок, Паскаль; Эйде, Эрик; Эллисон, Чаки; Ян, Сюэджун (2012). «Уменьшение количества тестовых примеров для ошибок компилятора C». Материалы 33-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . ПЛДИ '12. Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 335–346. дои : 10.1145/2254064.2254104 . ISBN 9781450312059 . S2CID 1025409 .