Huỳnh Tấn Khải * , Quản Thành Thơ , Bùi Hoài Thắng Nguyễn Minh Thông

* Tác giả liên hệ (htkhai@nomail.com)

Abstract

To help programmers quickly develop their software systems, research communities have proposed some approaches for automatic search of function APIs, mostly based on keywords used in the API descriptions. However, the accuracy of those approaches is still limited. Formal specification with the rigor of the syntax and semantics can be applied to improve the research results of this direction. In this paper, we firstly present a survey on formal specification techniques for software design. Next, we propose a framework for searching and reusing API functions automatically based on formal specification described by JML. In addition, the framework also supports automatic composition of API functions to meet the requirement demand. Some case studies are also presented to imply the practical potential of our approach.
Keywords: Automatic API functions searching, automatic function composition, component reuse, formal specification, design by contract

Tóm tắt

Để giúp cho các lập trình viên phát triển nhanh hệ thống phần mềm của họ, cộng đồng nghiên cứu đã đề xuất một số cách tiếp cận cho việc tìm kiếm tự động các hàm API. Hầu hết các nghiên cứu này đều dựa trên các từ khóa được sử dụng trong các mô tả của các hàm API. Tuy nhiên, độ chính xác của các hướng tiếp cận này vẫn còn hạn chế. Đặc tả hình thức với sự chặt chẽ trong cú pháp và ngữ nghĩa có thể được áp dụng để cải thiện kết quả của các hướng nghiên cứu này. Trong bài báo này, đầu tiên, chúng tôi trình bày một khảo sát về các kỹ thuật đặc tả hình thức cho thiết kế phần mềm. Tiếp theo, chúng tôi đề xuất một khung thức cho việc tìm kiếm và tái sử dụng các hàm API tự động dựa trên đặc tả chính thức được mô tả bởi JML. Ngoài ra, khung thức còn hỗ trợ việc tổ hợp tự động các hàm API để đáp ứng các yêu cầu phần mềm. Một số kết quả thử nghiệm cũng được trình bày để cho thấy khả năng thực tế trong hướng tiếp cận của chúng tôi.
Từ khóa: Tìm kiếm hàm tự động, gọi hàm tự động, tái sử dụng thành phần, đặc tả hình thức, thiết kế thoả thuận

Article Details

Tài liệu tham khảo

M. D. McIlroy, J. M. Buxton, P. Naur and B. Randell, 1968. Mass-produced software components. In Proceedings of the 1st International Conference on Software Engineering, pp: 88–98.

Sametinger, Johannes, 1997. Software engineering with reusable components. Springer, pp: 11-15.

Tran DinhHuy and HuaPhung Nguyen, 2013. API specification-based function search engine using natural language query. Computing, Management and Telecommunications, International Conference on IEEE, pp:140-145.

Hoffmann, Raphael, J. Fogarty, and D.S. Weld, 2007. Assieme: finding and leveraging implicit references in a web search interface for programmers. Proc. of the 20th annual ACM symposium on User interface software, pp:13-22.

Chatterjee, Shaunak, S. Juvekar, and K. Sen, 2009. Sniff: A search engine for java using free-form queries. In: Fundamental Approaches to Software Engineering. Springer Berlin Heidelberg, pp: 385-400.

B. Randell, 1973. The Origin of Digital Computers. Springer-Verlag, p. 298.

Meyer, Bertrand, 2002. Design by Contract. Prentice Hall.

D.S. Weld, 1999. Recent Advances in AI Planning. AI Magazine, Vol.20: 2-93.

R. Floyd, 1976. Assigning Meanings to Programs. In Mathematical Aspects of Computer Science. Proc. Syrup. Appl. Maths. Vol.19:19-32.

C.A.R. Hoare, 1969. An Axiomatic Basis for Computer Programming. In: Comm. ACM, Vol. 12: 576-583.

P. Naur, 1969. Proofs of algorithms by General Snapshots. BIT Numerical Mathematics. Vol.6.4: 310-316.

E.M. Clarke, J.M. Wing et al, 1996. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, Vol.28: 626-643.

J.M. Wing, J. Woodcock and J. Davies, 1999. FM-99: Worm Conference on Formal Methods in the Development of Computing Systems. LNCS 1708 and 1709, Springer-Verlag.

Burdy, Lilian, et al., 2005. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer. Vol.7: 212-232.

J.V. Guttag and J.J. Horning, 1993. LARCH: Languages and Tools for Formal Specification. Springer-Verlag.

Jacobs, Bart, and E. Poll, 2001. A logic for the Java Modeling Language JML. Springer Berlin.

Barnett, et.al, 2005. The Spec# programming system: An overview. Construction and analysis of safe, secure, and interoperable smart devices. Springer Berlin Heidelberg, pp:49-69.

Barnett, Mike, et al., 2006. Boogie: A modular reusable verifier for object-oriented programs. Formal methods for Components and Objects. Springer Berlin Heidelberg. pp: 364-387.

Gopan, Denis, and Thomas, 2007. Guided static analysis. In: Static Analysis, Springer Berlin Heidelberg, pp: 349-365.

L. Correnson, et al., 2013. Frama-C User Manual, Software Safety Laboratory, Saclay.

P. Baudin, et.al, 2012. ACSL: ANSI/ISO C Specification Language. Version 1.6.

Kuncak, Viktor, and M. Rinard, 2006. An overview of the Jahob analysis system: project goals and current status. In: Parallel and Distributed Processing Symposium. 8 pp

Watt, A. David, B.A. Wichmann and W. Findlay, 1987. Ada language and methodology. Prentice Hall International (UK).

Barnes and John, 2011. Rationale for Ada 2012: Contracts and aspects. ADA USER, Vol.32 (4): 247-264.

C. Flanagan, et.al, 2002. Extended static checking for Java. Proc. of the Conference on Programming Language Design and Implementation, pp: 234-245.

Beckert, Bernhard, R. Hähnle, and P.H. Schmitt, 2007. Verification of object-oriented software: The KeY approach. Springer-Verlag.

Rish, Irina. An empirical study of the naive Bayes classifier. IJCAI 2001 workshop on empirical methods in artificial intelligence. Vol.3: 41-46.