maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2016-6-754-766mais-412Research ArticleОригинальные статьиArticlesФормализм и языковые инструменты для описания семантики программных библиотекThe Formalism and Language Tools for Semantics Specification of Software Librarieshttps://orcid.org/0000-0003-0276-4517ИцыксонВ. М.ItsyksonV. M.

канд. техн. наук, доцент, ул. Политехническая, д. 29, г. Санкт-Петербург, 195251, Россия

PhD, 29 Polytechnicheskaya str., Saint-Petersburg 195251, Russia

vlad@icc.spbstu.ruСанкт-Петербургский политехнический университет Петра ВеликогоРоссияPeter the Great St. Petersburg Polytechnic UniversityRussian Federation201620122016236754766Copyright © Ицыксон В.М., 20162016Ицыксон В.М.Itsykson V.M.Данная работа распространяется под лицензией 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/412

Статья посвящена вопросам спецификации структуры и поведения программных библиотек. Описываются существующие проблемы спецификации библиотек. Дается краткий обзор состояния дел в области формализации спецификации библиотек и библиотечных функций. Формулируются требования к создаваемому формализму. На основе требований предлагается формализм, позволяющий специфицировать все необходимые свойства библиотек, требуемые для автоматизации нескольких классов задач: обнаружение дефектов в программном обеспечении, миграция приложений в новое окружение, генерация программной документации. На базе формализма формулируются требования к языковым средствам спецификации библиотек. В заключении определяются дальнейшие направления исследований.

The paper is dedicated to the specification of the structure and the behaviour of soft-ware libraries. It describes the existing problems of libraries specifications. A brief overview of the research field concerned with formalizing the specification of libraries and library functions is presented. The requirements imposed on the formalism designed are established; the formalism based on these requirements allows specifying all the properties of the libraries needed for automation of several classes of problems: defects detection in the software, migration of applications into a new environment, gen-eration of software documentation. The requirements on the language tools based on the developed formalism are proposed. The conclusion defines potential directions for further research.

формальная спецификацияпрограммная библиотекаповеденческое описаниепрограммный дефектязык спецификацийformal specificationsoftware librarybehavioral descriptionsoftware defectspecification languageReferencesLamb D., “IDL: sharing intermediate representations”, ACM Trans. Program. Lang. Syst, 9:3 (1987), 297–318.Lamb D., “IDL: sharing intermediate representations”, ACM Trans. Program. Lang. Syst, 9:3 (1987), 297–318.Exton C., Watkins D., Thompson D., “Comparisons between CORBA IDL and COM/DCOM MIDL: Interfaces for Distributed Computing”, Proceedings of the Technology of Object- Oriented Languages and Systems – Tools-25 (TOOLS ’97), IEEE Computer Society, Washington, DC, USA, 1997, 15–23.Exton C., Watkins D., Thompson D., “Comparisons between CORBA IDL and COM/DCOM MIDL: Interfaces for Distributed Computing”, Proceedings of the Technology of Object- Oriented Languages and Systems – Tools-25 (TOOLS ’97), IEEE Computer Society, Washington, DC, USA, 1997, 15–23.Sankar S., Hayes R., “ADL—an interface definition language for specifying and testing software”, SIGPLAN, 29:8 (1994), 13–21.Sankar S., Hayes R., “ADL—an interface definition language for specifying and testing software”, SIGPLAN, 29:8 (1994), 13–21.Allen R., Garlan D., “Formalizing architectural connection”, Proceedings of the 16th international conference on Software engineering (ICSE ’94), IEEE Computer Society Press, Los Alamitos, CA, USA, 1994, 71–80.Allen R., Garlan D., “Formalizing architectural connection”, Proceedings of the 16th international conference on Software engineering (ICSE ’94), IEEE Computer Society Press, Los Alamitos, CA, USA, 1994, 71–80.Хоар Ч., Взаимодействующие последовательные процессы, М.: Мир, 1989.Hoar C.A.R., Communicating sequential processes, Mir, Moscow, 1989, (in Russian).Roscoe A.W., “Modelling and verifying key-exchange protocols using CSP and FDR”, Proceedings of 1995 IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, 1995.Roscoe A.W., “Modelling and verifying key-exchange protocols using CSP and FDR”, Proceedings of 1995 IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, 1995.de Alfaro L, Henzinger T., “Interface automata”, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering (ESEC/FSE-9), ACM, New York, NY, USA, 2001, 109–120.de Alfaro L, Henzinger T., “Interface automata”, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering (ESEC/FSE-9), ACM, New York, NY, USA, 2001, 109–120.Ramanathan M., Grama A., Jagannathan S., “Static specification inference using predicate mining”, Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’07), ACM, New York, USA, 2007, 123–134.Ramanathan M., Grama A., Jagannathan S., “Static specification inference using predicate mining”, Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’07), ACM, New York, USA, 2007, 123–134.Sankaranarayanan S.,Ivancic F.,Gupta A., “Mining library specifications using inductive logic programming”, Proceedings of the 30th international conference on Software engineering (ICSE ’08), ACM, New York, USA, 2008, 131–140.Sankaranarayanan S.,Ivancic F.,Gupta A., “Mining library specifications using inductive logic programming”, Proceedings of the 30th international conference on Software engineering (ICSE ’08), ACM, New York, USA, 2008, 131–140.Ball T., Rajamani S.K., SLIC: a Specication Language for Interface Checking (of C), Microsoft Research, Technical Report, MSR-TR-2001-21, 2002.Ball T., Rajamani S.K., SLIC: a Specication Language for Interface Checking (of C), Microsoft Research, Technical Report, MSR-TR-2001-21, 2002.Leavens G.T., “The future of library specification”, Proceedings of the FSE/SDP workshop on Future of software engineering research (FoSER ’10), ACM, New York, USA, 2010, 211–216.Leavens G.T., “The future of library specification”, Proceedings of the FSE/SDP workshop on Future of software engineering research (FoSER ’10), ACM, New York, USA, 2010, 211–216.Ицыксон В.М., Зозуля А.В., “Формализм для описания частичных спецификаций компонентов программного окружения”, Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление, 4 (2011), 81–90.Itsykson V.M., Zozulya A.V., “The formalism for description of the partial specifications of program envinroment components”, St. Petersburg State Polytechnical University Journal. Computer Science. Telecommunication and Control Systems, 4 (2011), 81–90, (in Russian).Ицыксон В.М., Глухих М.И., “Язык спецификаций поведения программных компонентов”, Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление, 3 (2010), 63–71.Itsykson V.M., Glukhikh M.I., “A program component behavior specification language”, St. Petersburg State Polytechnical University Journal. Computer Science. Telecommunication and Control Systems, 3 (2010), 63–71, (in Russian).Akhin M.Kh., Belyaev M.A., Itsykson V.M., “Software defect detection by combining bounded model checking and approximations of functions”, Automatic Control and Computer Sciences, 48:7 (2014), 389–397.Akhin M.Kh., Belyaev M.A., Itsykson V.M., “Software defect detection by combining bounded model checking and approximations of functions”, Automatic Control and Computer Sciences, 48:7 (2014), 389–397.Itsykson V., etc, “Automatic defects detection in industrial C/C++ software”, Proceeding of 5th Central and Eastern European Software Engineering Conference in Russia (CEE- SECR), IEEE, 2009, 50–55.Itsykson V., etc, “Automatic defects detection in industrial C/C++ software”, Proceeding of 5th Central and Eastern European Software Engineering Conference in Russia (CEE- SECR), IEEE, 2009, 50–55.Ицыксон В.М., Зозуля А.В., “Автоматизированная трансформация программ при миграции на новые библиотеки”, Программная инженерия, 6 (2012), 8–14.Itsykson V.M., Zozulya A.V., “Automated Program Transformation for Migration to New Libraries”, Software Engineering, 6 (2012), 8–14, (in Russian).Kirchner F., etc, “Frama-C: A software analysis perspective”, Formal Aspects of Computing, 27:3 (2015), 5733609.Kirchner F., etc, “Frama-C: A software analysis perspective”, Formal Aspects of Computing, 27:3 (2015), 5733609.

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