Верификация преобразования грамматики в нормальную форму Хомского в F

Сертификационное программирование позволяет доказывать, что программа соответствует своему формальному описанию. Проверка корректности производится статически, благодаря чему становится возможным отказаться от дальнейшего тестирования проверифицированных программ. Среди инструментов, предназначенных для сертификационного программирования, только инструмент F* позволяет реализовывать программы на языке общего назначения и автоматизирует доказательство их корректности. Последнее означает, что инструмент F* автоматически выведет доказательство корректности, где это возможно, при этом пользователь может специфицировать более сложные доказательства, если это необходимо. Мы работаем над применением данного подхода к проекту YaccConstructor - платформе для исследования и разработки генераторов лексических и синтаксических анализаторов и других алгоритмов для работы с грамматиками. В данной статье рассматривается верификация реализации одного из таких алгоритмов - преобразования грамматики в нормальную форму Хомского - что является первой задачей на пути к верификации всего проекта YaccConstructor. Для программы, реализующей данное преобразование, доказаны завершаемость и тотальность, а также установлен порядок применения используемых в ней основных преобразований с использованием зависимых и уточняющих типов. Следующим важным направлением данной работы является доказательство эквивалентности исходной и преобразованной грамматик. Инструмент F* позволяет извлекать код, написанный на F*, как программу на языке программирования F# или OCaml. Так как F# является основным языком разработки проекта YaccConstructor, это позволит сохранить совместимость проверифицированных программ с существующими в проекте. В статье сформулированы преимущества и недостатки применения инструмента F*.

сертификационное программирование, F*, верификация программ, контекстно-свободная грамматика, нормальная форма Хомского, преобразование грамматики, dependent type, refinement type

1. H. Geuvers. Proof assistants: History, ideas and future. Sadhana, 2009, vol. 34, issue 1. pp. 3–25. DOI: 10.1007/s12046-009-0001-5.

2. A. Chlipala. Certified programming with dependent types. MIT Press, 2013, 440 p.

3. T. Sheard, A. Stump, S. Weirich. Language-based verification will change the world. Proceedings of the FSE/SDP workshop on Future of software engineering research, 2010, pp. 343–348. DOI: 10.1145/1882362.1882432.

4. E. Tanter, N. Tabareau. Gradual certified programming in Coq. Proceedings of the 11th Symposium on Dynamic Languages, 2015. pp. 26–40. DOI: 10.1145/2816707.2816710.

5. The Coq proof assistant. June 2016. https://coq.inria.fr/

6. U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, 2007.

7. The F* homepage. June 2016. https://www.fstar-lang.org/

8. E. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 2013, vol. 23, n. 5, pp. 552–593. DOI: 10.1017/S095679681300018X.

9. N. Swamy, C. Hritcu, C. Keller. Dependent Types and Multi-monadic Effects in F*. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016, pp. 256–270. DOI: 10.1145/2837614.2837655

10. The YaccConstructor homepage. June 2016. https://github.com/YaccConstructor/

11. I. Kirilenko, S. Grigorev, D. Avdiukhin. Syntax analyzers development in automated reengineering of informational system. St. Petersburg State Polytechnical University Journal. Computer Science. Telecommunications and Control Systems, 2013, no. 174, pp. 94 – 98.

12. J.-H. Jourdan, F. Pottier, X. Leroy. Validating LR (1) parsers. Programming Languages and Systems, 2012, pp. 397–416.

13. K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. International Conference on Logic for Programming Artificial Intelligence and Reasoning, 2010, pp. 348–370.

14. J.-C. Filliatre, A. Paskevich. Why3: Where Programs Meet Provers. Proceedings of the 22Nd European Conference on Programming Languages and Systems, 2013, pp. 125–128. DOI: 10.1007/978-3-642-37036-6_8.

15. B. C. Pierce. Types and Programming Languages. MIT Press, 2002, 645 p.

16. F* tutorial. June 2016. https://www.fstar-lang.org/tutorial/

17. D. Syme, A. Granicz, A. Cisternino. Expert F#. Apress, 2012, 609 p.

18. D. Firsov, T. Uustalu. Certified normalization of context-free grammars. Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015, pp. 167–174. DOI: 10.1145/2676724.2693177.

19. Verification of grammar transformation to Chomsky normal form in F*. June 2016. https://github.com/YaccConstructor/YC_FStar.