Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

Официальная проверка [ править ]

Два основных формальных подхода к проверке правильности компиляции - это подтверждение правильности компилятора для всех входных данных и подтверждение правильности компиляции конкретной программы (проверка перевода).

Корректность компилятора для всех входных программ [ править ]

Проверка компилятора с помощью формальных методов включает длинную цепочку формальной дедуктивной логики . [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] и Cobol [15] .

Другими распространенными методами тестирования компиляторов являются фаззинг [16] (который генерирует случайные программы для поиска ошибок в компиляторе) и сокращение тестовых примеров (которое пытается минимизировать найденный тестовый пример, чтобы облегчить понимание). [17]

См. Также [ править ]

  • Компилятор
  • Проверка и валидация (программное обеспечение)
  • Корректность (информатика)
  • Компилятор CompCert C - официально проверенный компилятор C
  • Размышления о доверии

Ссылки [ править ]

  1. ^ Де Милло, РА; Lipton, RJ; Перлис, AJ (1979). «Социальные процессы и доказательства теорем и программ». Коммуникации ACM . 22 (5): 271–280. DOI : 10.1145 / 359104.359106 .
  2. Перейти ↑ Leroy, X. (2006). «Формальная сертификация серверной части компилятора или: программирование компилятора с помощью Proof Assistant». Уведомления ACM SIGPLAN . 41 : 42–54. DOI : 10.1145 / 1111320.1111042 .
  3. ^ Лерой, Ксавье (2009-12-01). «Формально проверенная серверная часть компилятора». Журнал автоматизированных рассуждений . 43 (4): 363–446. arXiv : 0902.2137 . DOI : 10.1007 / s10817-009-9155-4 . ISSN 0168-7433 . 
  4. ^ "CompCert - Компилятор CompCert C" . compcert.inria.fr . Проверено 21 июля 2017 .
  5. ^ «CakeML: Проверенная реализация ML» .
  6. ^ Стефан Диль, Генерация компиляторов и абстрактных машин ,ориентированная на естественную семантику , Формальные аспекты вычислений, Vol. 12 (2), Springer Verlag, 2000. doi : 10.1007 / PL00003929
  7. ^ Пнуэли, Амир; Сигель, Майкл; Зингерман, Эли. Проверка перевода . Инструменты и алгоритмы для построения и анализа систем, 4-я Международная конференция, TACAS '98.
  8. ^ Компиляторы: принципы, методы и инструменты , инфра 1986, стр. 731.
  9. ^ там же, 2006, стр. 16.
  10. ^ Кристофер Фрейзер; Дэвид Хэнсон (1995). Компилятор C с возможностью перенастройки: дизайн и реализация . Бенджамин / Каммингс Паблишинг. ISBN 978-0-8053-1670-4., стр. 531–3.
  11. ^ Марк У. Бейли; Джек В. Дэвидсон (2003). «Автоматическое обнаружение и диагностика ошибок в сгенерированном коде для вызова процедур» (PDF) . IEEE Transactions по разработке программного обеспечения . 29 (11): 1031–1042. CiteSeerX 10.1.1.15.4829 . DOI : 10.1109 / tse.2003.1245304 . Архивировано из оригинального (PDF) 28 апреля 2003 года . Проверено 24 марта 2009 .   , п. 1040.
  12. ^ Например, Кристиан Линдиг (2005). «Случайное тестирование соглашений о вызовах C» (PDF) . Материалы Шестого международного семинара по автоматизированной отладке . ACM. ISBN  1-59593-050-7. Архивировано из оригинального (PDF) 11 июля 2011 года . Проверено 24 марта 2009 ., и Эрик Эйде; Джон Регер (2008). «Volatiles неправильно скомпилированы, и что с этим делать» (PDF) . Материалы 7-й международной конференции ACM по встроенному ПО . ACM. ISBN  978-1-60558-468-3. Проверено 24 марта 2009 .
  13. ^ Флэш Шеридан (2007). «Практическое тестирование компилятора C99 с использованием сравнения выходных данных» (PDF) . Программное обеспечение: практика и опыт . 37 (14): 1475–1488. DOI : 10.1002 / spe.812 . Проверено 24 марта 2009 . Библиография на http://pobox.com/~flash/compiler_testing_bibliography.html . Проверено 13 марта 2009 . Отсутствует или пусто |title=( справка ) .
  14. ^ "Источник пакета проверки Fortran" . Проверено 1 сентября 2011 .
  15. ^ "Источник пакета проверки Cobol" . Проверено 1 сентября 2011 .
  16. ^ Чен, Ян; Groce, Алекс; Чжан, Чаоцян; Вонг, Вен-Кин; Папоротник, Сяоли; Эйде, Эрик; Регер, Джон (2013). Укрощение фаззеров компилятора . Труды 34-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . PLDI '13. Нью-Йорк, Нью-Йорк, США: ACM. С. 197–208. CiteSeerX 10.1.1.308.5541 . DOI : 10.1145 / 2491956.2462173 . ISBN  9781450320146.
  17. ^ Регер, Джон; Чен, Ян; Куок, Паскаль; Эйде, Эрик; Эллисон, Чаки; Ян, Сюэцзюнь (2012). Снижение испытаний случае компилятор Си ошибок . Труды 33-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . PLDI '12. Нью-Йорк, Нью-Йорк, США: ACM. С. 335–346. DOI : 10.1145 / 2254064.2254104 . ISBN 9781450312059.
  • v
  • т
  • е