Skip to content

Latest commit

 

History

History
39 lines (25 loc) · 3.69 KB

verification.md

File metadata and controls

39 lines (25 loc) · 3.69 KB
Raw

Формальная верификация

Daniel Patterson and Amal Ahmed, The Next 700 Compiler Correctness Theorems

Комментарий @gabriel-fallen

Почти 30 страниц (считая список литературы), посвящённых проблеме формальной корректности раздельной компиляции.

Статья описывает спектр возможных теорем о корректности, как для whole-program, так и раздельной компиляции, и презентует обобщённый фреймворк, в который их можно поместить.

Рассматриваются четыре возможных сеттинга верифицированной раздельной компиляции:

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

Через эту призму авторы делают обзор большей части существующей литературы и результатов по части верифицированной компиляции, как раздельной так и нет. Поэтому статья может служить отличным введением в проблематику и знакомством с этой областью исследований.

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

A Survey of Compiler Testing Junjie Chen, Jibesh Patra, Michael Pradel, Yingfei Xiong, Hongyu Zhang, Dan Hao, Lu Zhang ACM Computing Surveys Vol 53 Issue 1 Article No.: 4 pp 1–36, 2020

https://dl.acm.org/doi/10.1145/3363562

Комментарий от @ksromanov. Просто читаемый свежий обзор методов тестирования компиляторов. Статья охватывает тему с разных сторон, включая

  • построение тестовых наборов программ
  • определение того, ошибочна или нет компиляция
  • оптимизация процесса тестирования
  • обработка результатов тестирования

Статья хорошо классифицирует подходы генерации тестовых программ, давая широкий обзор существующих проектов как по методикам генерации, так и по целевым языкам программирования.

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