Geodesic
The formalism and language tools for semantics specification of software libraries
Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 754-766.

Voir la notice de l'article provenant de la source Math-Net.Ru

The paper is dedicated to the specification of the structure and the behaviour of software 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, generation of software documentation. The requirements on the language tools based on the developed formalism are proposed. The conclusion defines potential directions for further research.
Keywords: formal specification, software library, behavioral description, software defect, specification language. 
@article{MAIS_2016_23_6_a6,
     author = {V. M. Itsykson},
     title = {The formalism and language tools for semantics specification of software libraries},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {754--766},
     publisher = {mathdoc},
     volume = {23},
     number = {6},
     year = {2016},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a6/}
}
TY  - JOUR
AU  - V. M. Itsykson
TI  - The formalism and language tools for semantics specification of software libraries
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2016
SP  - 754
EP  - 766
VL  - 23
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a6/
LA  - ru
ID  - MAIS_2016_23_6_a6
ER  - 
%0 Journal Article
%A V. M. Itsykson
%T The formalism and language tools for semantics specification of software libraries
%J Modelirovanie i analiz informacionnyh sistem
%D 2016
%P 754-766
%V 23
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a6/
%G ru
%F MAIS_2016_23_6_a6
V. M. Itsykson. The formalism and language tools for semantics specification of software libraries. Modelirovanie i analiz informacionnyh sistem, Tome 23 (2016) no. 6, pp. 754-766. http://geodesic.mathdoc.fr/item/MAIS_2016_23_6_a6/

[1] Lamb D., “IDL: sharing intermediate representations”, ACM Trans. Program. Lang. Syst, 9:3 (1987), 297–318 | DOI

[2] 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 (Washington, DC, USA, 1997), IEEE Computer Society, 15–23

[3] Sankar S., Hayes R., “ADL-an interface definition language for specifying and testing software”, SIGPLAN, 29:8 (1994), 13–21 | DOI

[4] Allen R., Garlan D., “Formalizing architectural connection”, Proceedings of the 16th international conference on Software engineering, ICSE '94 (Los Alamitos, CA, USA, 1994), IEEE Computer Society Press, 71–80

[5] Hoar C. A. R., Communicating sequential processes, Mir, M., 1989 (in Russian)

[6] 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

[7] 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 (New York, NY, USA, 2001), ACM, 109–120

[8] 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 (New York, USA, 2007), ACM, 123–134

[9] Sankaranarayanan S., Ivancic F., Gupta A., “Mining library specifications using inductive logic programming”, Proceedings of the 30th international conference on Software engineering, ICSE '08 (New York, USA, 2008), ACM, 131–140 | MR

[10] Ball T., Rajamani S. K., SLIC: a Specication Language for Interface Checking (of C), Microsoft Research, Technical Report, MSR-TR-2001-21, 2002

[11] Leavens G. T., “The future of library specification”, Proceedings of the FSE/SDP workshop on Future of software engineering research, FoSER '10 (New York, USA, 2010), ACM, 211–216

[12] 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, 2011, no. 4, 81–90 (in Russian)

[13] Itsykson V. M., Glukhikh M. I., “A program component behavior specification language”, St. Petersburg State Polytechnical University Journal. Computer Science. Telecommunication and Control Systems, 2010, no. 3, 63–71 (in Russian) | MR

[14] 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 | DOI

[15] 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

[16] Itsykson V. M., Zozulya A. V., “Automated Program Transformation for Migration to New Libraries”, Software Engineering, 6 (2012), 8–14 (in Russian)

[17] Kirchner F., etc, “Frama-C: A software analysis perspective”, Formal Aspects of Computing, 27:3 (2015), 573–609 | DOI | MR