Прототип статического тайп-чекера для языка программирования Jolie
Даниэль де Карвальо,
Мануэль Маццара,
Богдан Мингела,
Лариса Сафина,
Александр Чичигин,
Николай Трошков https://doi.org/10.18255/1818-1015-2017-6-704-717
Аннотация
Статическая верификация исходного кода программы является важным элементом надежности программного обеспечения. Под верификацией предполагается доказательство соответствия поведения программы ее спецификации. Во многих языках программирования используется как статическая, так и динамическая проверка типов. Таким образом, статический тайп-чекер старается проверить все возможное во время компиляции, а динамический проверяет оставшееся. На данный момент язык программирования Jolie имеет динамическую систему типов, что позволяет обнаруживать ошибки только во время выполнения программы. Статическая система типов для языка была формально определена на бумаге, но пока не реализована. В этой статье мы представим прототип статического тайп-чекера для языка программирования Jolie (JolieStaticTypeChecker или JSTC), основанный на SMT-решателе. Мы опишем базовую теорию, необходимую для реализации тайп-чекера, саму реализацию, а также процесс статического анализа программы. Статья публикуется в авторской редакции.
Об авторах
Даниэль де Карвальо
Университет Иннополис
Россия
доцент
Россия
доцент
Мануэль Маццара
Университет Иннополис
Россия
руководитель лаборатории архитектуры и моделей ПО
Россия
руководитель лаборатории архитектуры и моделей ПО
Богдан Мингела
Университет Иннополис
Россия
студент
Россия
студент
Лариса Сафина
Университет Иннополис
Россия
младший научный сотрудник лаборатории архитектуры и моделей ПО
Россия
младший научный сотрудник лаборатории архитектуры и моделей ПО
Александр Чичигин
Университет Иннополис
Россия
ООО Тайпэбл
Россия
ООО Тайпэбл
Николай Трошков
Университет Иннополис
Россия
студент
Россия
студент
Список литературы
1. Akentev E., Tchitchigin A., Safina L., Mazzara M., “Verified type checker for Jolie programming language”, https://arxiv.org/pdf/1703.05186.pdf.
2. Bandura A., Kurilenko N., Mazzara M., Rivera V., Safina L., Tchitchigin A., “Jolie Community on the Rise”, 9th IEEE International Conference on Service-Oriented Computing and Applications, SOCA, 2016.
3. Barrett C., Stump A., Tinelli C., “The SMT-LIB Standard. Version 2.0”, Proceedings of the 8th international workshop on satisfiability modulo theories, Edinburgh, England, 2010.
4. Cardelli L., “Type Systems”, ACM Computing Surveys, 28 (1996), 263–264.
5. Dragoni N., Dustdar S., Larsen S. T., Mazzara M., “Microservices: Migration of a Mission Critical System”, https://arxiv.org/abs/1704.04173.
6. Dragoni N., Giallorenzo S., Lluch-Lafuente A., Mazzara M., Montesi F., Mustafin R., Safina L., “Microservices: yesterday, today, and tomorrow”, Present and Ulterior Software Engineering, ed. Bertrand Meyer, Manuel Mazzara, Springer, 2017, 195–216.
7. Dragoni N., Lanese I., Larsen S. T., Mazzara M., Mustafin R., Safina L., “Microservices: How To Make Your Application Scale”, A.P. Ershov Informatics Conference (the PSI Conference Series, 11th edition), Lecture Notes in Computer Science, Springer, 2017.
8. Gmehlich R., Grau K., Loesch F., Iliasov A., Jackson M., Mazzara M., “Towards a formalism-based toolkit for automotive applications”, 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE 2013), IEEE Computer Society, 2013, 36–42.
9. Guidi C., Lanese I., Mazzara M., Montesi F., “Microservices: a Language-based Approach”, Present and Ulterior Software Engineering, ed. Bertrand Meyer, Manuel Mazzara, Springer, 2017, 217–225.
10. Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 12 (1969), 576–583.
11. Jhala R., “Liquid Haskell”, https://ucsd-progsys.github.io/liquidhaskell-blog/.
12. MacKenzie M. C., Laskey K., McCabe F., Brown P. F., Metz R., “Reference model for service oriented architecture 1.0”, OASIS Standard, 12 (2006).
13. Mazzara M., Towards Abstractions for Web Services Composition, Ph.D. Thesis, University of Bologna, 2006, http://www.informatica.unibo.it/it/ricerca/technical-report/ 2006/UBLCS-2006-08.
14. Mazzara M., Abouzaid F., Dragoni N., Bhattacharyya A., “Toward Design, Modelling and Analysis of Dynamic Workflow Reconfigurations – A Process Algebra Perspective”, Web Services and Formal Methods, 8th International Workshop, WS-FM 2011, Lecture Notes in Computer Science, 7176, 2011, 64–78.
15. Mazzara M., Abouzaid F., Dragoni N., Bhattacharyya A., “Design, Modelling and Analysis of a Workflow Reconfiguration”, Proceedings of the International Workshop on Petri Nets and Software Engineering, Newcastle upon Tyne, UK, June 20–21, 2011, 10–24.
16. Mazzara M., Biselli L., Greco P. P., Dragoni N., Marra˙a A., Qamar N., Simona de Nicola, “Social networks and collective intelligence: a return to the agora”, Social Network Engineering for Secure Web Data and Services, IGI Global, 2013.
17. Mazzara M., Mustafin R., Safina L., Lanese I., “Towards Microservices and Beyond: An incoming Paradigm Shift in Distributed Computing”, https://arxiv.org/pdf/1610. 01778.pdf.
18. Milner R., Communication and concurrency, Prentice Hall International (UK) Ltd., 1995.
19. Milner R., Communicating and Mobile Systems: The ˇ-calculus, Cambridge University Press, 1999.
20. Montesi F., Guidi C., Zavattaro G., “Service-Oriented Programming with Jolie”, Web Services Foundations, Springer, 2014, 81–107.
21. Moura de L., Bjørner N., “Z3: An E˚cient SMT Solver”, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008 (Budapest, Hungary, March 29–April 6, 2008), Lecture Notes in Computer Science, 4963, Springer, 2008, 337–340.
22. Moura de L., Bjørner N., “Satisfiability modulo theories: An appetizer”, Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Lecture Notes in Computer Science, 5902, Springer, 2009, 23–36.
23. Nalin M., Baroni I., Mazzara M., “A Holistic Infrastructure to Support Elderlies’ Independent Living”, Encyclopedia of E-Health and Telemedicine, IGI-Global, 2016, 591–605.
24. Newman S., Building microservices, O’Reilly Media, Inc., 2015.
25. Nielsen J. M., A Type System for the Jolie Language, Master thesis, Technical University of Denmark, 2013.
26. Rice H. G., “Classes of Recursively Enumerable Sets and Their Decision Problems”, Trans. Amer. Math. Soc., 74 (1953), 358–366.
27. Rondon P. M., Kawaguci M., Jhala R., “Liquid Types”, SIGPLAN Not., 43:6 (2008), 159– 169.
28. Safina L., Mazzara M., Montesi F., Rivera V., “Data-driven Workflows for Microservices (genericity in Jolie)”, Proc. of the 30th IEEE International Conference on Advanced Information Networking and Applications (AINA 2016), 2016.
29. Salikhov D., Khanda K., Gusmanov K., Mazzara M., Mavridis N., “Microservice-based IoT for Smart Buildings”, Proceedings of the 31st International Conference on Advanced Information Networking and Applications Workshops (WAINA), 2017.
30. Salikhov D., Khanda K., Gusmanov K., Mazzara M., Mavridis N., “Jolie Good Buildings: Internet of things for smart building infrastructure supporting concurrent apps utilizing distributed microservices”, Proceedings of the 1st International conference on Convergent Cognitive Information Technologies, 2016.
31. Tchitchigin A., Safina L., Mazzara M., Elwakil M., Montesi F., Rivera V., “Refinement types in Jolie”, Spring/Summer Young Researchers Colloquium on Software Engineering, SYRCoSE, 2016.
32. Vallverdú J., Talanov M., Distefano S., Mazzara M., Tchitchigin A., Nurgaliev I., “A cognitive architecture for the implementation of emotions in computing systems”, Biologically Inspired Cognitive Architectures, 15 (2016), 34 – 40.
33. “Z3”, https://github.com/Z3Prover/z3.
34. “OASIS. Web Services Business Process Execution Language”, http://docs.oasis-open. org/wsbpel/2.0/wsbpel-specification-draft.html.
35. “Agda”, http://wiki.portal.chalmers.se/agda/pmwiki.php.
36. “F*”, https://www.fstar-lang.org/.
Рецензия
Для цитирования:
де Карвальо Д., Маццара М., Мингела Б., Сафина Л., Чичигин А., Трошков Н. Прототип статического тайп-чекера для языка программирования Jolie. Моделирование и анализ информационных систем. 2017;24(6):704-717. https://doi.org/10.18255/1818-1015-2017-6-704-717
For citation:
de Carvalho D., Mazzara M., Mingela B., Safina L., Tchitchigin A., Troshkov N. Jolie Static Type Checker: a Prototype. Modeling and Analysis of Information Systems. 2017;24(6):704-717. https://doi.org/10.18255/1818-1015-2017-6-704-717
Просмотров:
1279
Послать статью по эл. почте 