maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2017-6-704-717mais-608Research ArticleОригинальные статьиArticlesПрототип статического тайп-чекера для языка программирования JolieJolie Static Type Checker: a Prototypehttps://orcid.org/0000-0003-1473-8551де КарвальоДаниэльDe CarvalhoDaniel

доцент

PhD

d.carvalho@innopolis.ruhttps://orcid.org/0000-0002-3860-4948МаццараМануэльMazzaraManuel

руководитель лаборатории архитектуры и моделей ПО

PhD

m.mazzara@innopolis.ruhttps://orcid.org/0000-0003-1384-7078МингелаБогданMingelaBogdan

студент

student

b.mingela@innopolis.ruhttps://orcid.org/0000-0002-4490-7451СафинаЛарисаSafinaLarisa

младший научный сотрудник лаборатории архитектуры и моделей ПО

researcher

l.safina@innopolis.ruhttps://orcid.org/0000-0001-9286-6116ЧичигинАлександрTchitchiginAlexander

ООО Тайпэбл

sad.ronin@gmail.comhttps://orcid.org/0000-0002-5151-9940ТрошковНиколайTroshkovNikolay

студент

student

n.trshkv@gmail.comУниверситет ИннополисРоссияInnopolis UniversityRussian FederationУниверситет ИннополисРоссияTypeable.io LLCRussian Federation201718122017246704717Copyright © де Карвальо Д., Маццара М., Мингела Б., Сафина Л., Чичигин А., Трошков Н., 20172017де Карвальо Д., Маццара М., Мингела Б., Сафина Л., Чичигин А., Трошков Н.de Carvalho D., Mazzara M., Mingela B., Safina L., Tchitchigin A., Troshkov N.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/608

Статическая верификация исходного кода программы является важным элементом надежности программного обеспечения. Под верификацией предполагается доказательство соответствия поведения программы ее спецификации. Во многих языках программирования используется как статическая, так и динамическая проверка типов. Таким образом, статический тайп-чекер старается проверить все возможное во время компиляции, а динамический проверяет оставшееся. На данный момент язык программирования Jolie имеет динамическую систему типов, что позволяет обнаруживать ошибки только во время выполнения программы. Статическая система типов для языка была формально определена на бумаге, но пока не реализована. В этой статье мы представим прототип статического тайп-чекера для языка программирования Jolie (JolieStaticTypeChecker или JSTC), основанный на SMT-решателе. Мы опишем базовую теорию, необходимую для реализации тайп-чекера, саму реализацию, а также процесс статического анализа программы. Статья публикуется в авторской редакции.

Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both static and dynamic type checking. With such approach, the static type checker verifies everything possible at compile time, and the dynamic one checks the remaining. The current state of the Jolie programming language includes a dynamic type system. Consequently, it allows avoidable run-time errors. A static type system for the language has been formally defined on paper but lacks an implementation yet. In this paper, we describe a prototype of Jolie Static Type Checker (JSTC), which employs a technique based on a SMT solver. We describe the theory behind and the implementation, and the process of static analysis. The article is published in the authors’ wording.

 

микросервисыстатический анализ кодаязык программирования Joliemicroservicestatic analysisJolie programming languageReferencesAkentev E., Tchitchigin A., Safina L., Mazzara M., “Verified type checker for Jolie programming language”, https://arxiv.org/pdf/1703.05186.pdf.Akentev E., Tchitchigin A., Safina L., Mazzara M., “Verified type checker for Jolie programming language”, https://arxiv.org/pdf/1703.05186.pdf.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.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.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.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.Cardelli L., “Type Systems”, ACM Computing Surveys, 28 (1996), 263–264.Cardelli L., “Type Systems”, ACM Computing Surveys, 28 (1996), 263–264.Dragoni N., Dustdar S., Larsen S. T., Mazzara M., “Microservices: Migration of a Mission Critical System”, https://arxiv.org/abs/1704.04173.Dragoni N., Dustdar S., Larsen S. T., Mazzara M., “Microservices: Migration of a Mission Critical System”, https://arxiv.org/abs/1704.04173.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.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.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.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.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.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.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.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.Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 12 (1969), 576–583.Hoare C. A. R., “An Axiomatic Basis for Computer Programming”, Communications of the ACM, 12 (1969), 576–583.Jhala R., “Liquid Haskell”, https://ucsd-progsys.github.io/liquidhaskell-blog/.Jhala R., “Liquid Haskell”, https://ucsd-progsys.github.io/liquidhaskell-blog/.MacKenzie M. C., Laskey K., McCabe F., Brown P. F., Metz R., “Reference model for service oriented architecture 1.0”, OASIS Standard, 12 (2006).MacKenzie M. C., Laskey K., McCabe F., Brown P. F., Metz R., “Reference model for service oriented architecture 1.0”, OASIS Standard, 12 (2006).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.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.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.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.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.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.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.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.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.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.Milner R., Communication and concurrency, Prentice Hall International (UK) Ltd., 1995.Milner R., Communication and concurrency, Prentice Hall International (UK) Ltd., 1995.Milner R., Communicating and Mobile Systems: The ˇ-calculus, Cambridge University Press, 1999.Milner R., Communicating and Mobile Systems: The ˇ-calculus, Cambridge University Press, 1999.Montesi F., Guidi C., Zavattaro G., “Service-Oriented Programming with Jolie”, Web Services Foundations, Springer, 2014, 81–107.Montesi F., Guidi C., Zavattaro G., “Service-Oriented Programming with Jolie”, Web Services Foundations, Springer, 2014, 81–107.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.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.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.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.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.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.Newman S., Building microservices, O’Reilly Media, Inc., 2015.Newman S., Building microservices, O’Reilly Media, Inc., 2015.Nielsen J. M., A Type System for the Jolie Language, Master thesis, Technical University of Denmark, 2013.Nielsen J. M., A Type System for the Jolie Language, Master thesis, Technical University of Denmark, 2013.Rice H. G., “Classes of Recursively Enumerable Sets and Their Decision Problems”, Trans. Amer. Math. Soc., 74 (1953), 358–366.Rice H. G., “Classes of Recursively Enumerable Sets and Their Decision Problems”, Trans. Amer. Math. Soc., 74 (1953), 358–366.Rondon P. M., Kawaguci M., Jhala R., “Liquid Types”, SIGPLAN Not., 43:6 (2008), 159– 169.Rondon P. M., Kawaguci M., Jhala R., “Liquid Types”, SIGPLAN Not., 43:6 (2008), 159– 169.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.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.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.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.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.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.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.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.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.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.“Z3”, https://github.com/Z3Prover/z3.“Z3”, https://github.com/Z3Prover/z3.“OASIS. Web Services Business Process Execution Language”, http://docs.oasis-open. org/wsbpel/2.0/wsbpel-specification-draft.html.“OASIS. Web Services Business Process Execution Language”, http://docs.oasis-open. org/wsbpel/2.0/wsbpel-specification-draft.html.“Agda”, http://wiki.portal.chalmers.se/agda/pmwiki.php.“Agda”, http://wiki.portal.chalmers.se/agda/pmwiki.php.“F*”, https://www.fstar-lang.org/.“F*”, https://www.fstar-lang.org/.

The authors declare that there are no conflicts of interest present.