MộT KHUNG THứC TìM KIếM Và TáI Sử DụNG HàM API Tự ĐộNG DựA TRÊN ĐặC Tả HìNH THứC

- MỘT KHUNG THỨC TÌM KIẾM VÀ TÁI SỬ DỤNG HÀM API TỰ ĐỘNG DỰA TRÊN ĐẶC TẢ HÌNH THỨC.
- 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.
- Đặ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.
- Một trong những hướng tiếp cận có thể vượt qua các khó khăn trên là sử dụng các đặc tả hình thức (formal specification) [6] để tìm kiếm và tổng hợp các hàm thư viện.
- Với cách tiếp cận này, các đặc tả hình thức, thực chất là các mệnh đề logic, với sự hỗ trợ của các công cụ suy luận và chứng minh định lý có thể cho được một lời giải đúng và đầy đủ cho một yêu cầu tìm kiếm hàm thư viện..
- Bên cạnh đó, việc sử dụng ngôn ngữ đặc tả hình thức sẽ loại bỏ được tính nhập nhằng và đa nghĩa của ngôn ngữ tự nhiên.
- Trong các phương pháp phát triển phần mềm dựa trên đặc tả hình thức hiện nay thì phương pháp Design by contract (DBC) [7] nổi lên như một trong những phương pháp phát triển nhanh và chặt chẽ.
- Chúng tôi đưa ra một khảo sát chi tiết về các hướng tiếp cận đặc tả hình thức theo phương pháp “thoả thuận”..
- Chúng tôi đưa ra một khung thức để tự động tìm kiếm và tổng hợp các hàm API dựa trên các đặc tả hình thức theo phương pháp “thoả thuận”..
- Trong khung thức đề nghị, chúng tôi đưa ra hướng tiếp cận tính toán độ tương tự giữa các đặc tả hình thức của các API.
- Phần còn lại của bài báo này được tổ chức như sau: Phần 2 trình bày về các ngôn ngữ đặc tả hình thức theo phương pháp “thỏa thuận”.
- Phần 3 trình bày ý tưởng về khung thức cho việc tìm kiếm hàm tự động dựa trên đặc tả hình thức JML.
- 2 CÁC NGÔN NGỮ HÌNH THỨC ĐẶC TẢ THEO PHƯƠNG PHÁP THỎA THUẬN 2.1 Đặc tả hình thức và hướng tiếp cận thoả thuận.
- Đặc tả hình thức cho phần mềm đã được quan tâm từ lâu trong lĩnh vực khoa học máy tính.
- Vào cuối những năm 1960, Floyd, Hoare và Naur đề xuất kỹ thuật tiền đề để chứng minh sự nhất quán giữa các chương trình tuần tự và các mô tả của chúng, được gọi là các đặc tả .
- Sự quan tâm về các đặc tả hình thức và các ứng dụng đa dạng của chúng trong lĩnh vực công nghệ phần mềm đã phát triển liên tục cho đến hiện nay [12][13]..
- Hình 1: “Thỏa thuận” của phương thức sqrt được biểu diễn bằng ngôn ngữ JML 2.2 Các ngôn ngữ đặc tả hình thức theo hướng tiếp cận “thoả thuận”.
- 2.2.1 Ngôn ngữ JML.
- JML (Java Modeling Language) [14] là ngôn ngữ đặc tả hành vi, được sử dụng để đặc tả hành vi của các mô đun trong ngôn ngữ Java.
- Nó là sự kết hợp phương pháp “thỏa thuận” với phương pháp đặc tả dựa trên mô hình của ngôn ngữ Larch [15]..
- Các đặc tả JML được thêm vào mã Java dưới dạng các chú giải (annotation) bên trong các chú thích (comment).
- Ví dụ trong Hình 2 minh họa việc sử dụng JML đặc tả cho lớp Purse.
- Trong đó, trường balance được đặc tả với bất biến (invariant) là balance luôn trong đoạn từ 0 đến.
- Hình 2: Ví dụ minh họa về đặc tả JML Phương thức debit nhận vào đối số amount..
- Spec# [17] là một ngôn ngữ hình thức cho các.
- Spec# là ngôn ngữ đặc tả cho phép kiểm tra động cũng như kiểm tra tĩnh chương trình.
- Các đặc tả của Spec# cũng được biên dịch thành một phần của chương trình thực thi, trong đó.
- Nó cho phép kiểm tra các đặc tả theo kỹ thuật phân tích tĩnh [19]..
- Hình 3 minh họa về đặc tả của Spec# cho lớp ArrayList.
- Trong đó, phương thức Insert được đặc tả với các tiền điều kiện (requires), hậu điều kiện (ensures).
- Đặc biệt, Spec# còn cho phép các đặc tả có thể thừa kế lẫn nhau.
- Điều này giúp cho các đặc tả của Spec# rõ ràng, đáng tin cậy và dễ đọc hơn so với các ngôn ngữ đặc tả khác.
- Hình 3: Minh họa về đặc tả Spec#.
- 2.2.3 Frama-C và ngôn ngữ ACSL.
- Để được phân tích bởi Frama-C, các chương trình C cần được đặc tả bởi ngôn ngữ ACSL (ANSI/ISO C Specification Language) [21]..
- Đây là ngôn ngữ đặc tả hình thức cho phép chúng ta đặc tả các thuộc tính của một chương trình C.
- Hình 4: Minh họa về đặc tả ACSL Ngoài tiền và hậu điều kiện, ACSL còn hỗ trợ đặc tả bất biến cho các đối tượng và vòng lặp.
- Sử dụng Jahob, các nhà phát triển có thể chứng minh theo phương pháp phân tích tĩnh rằng các phương thức hiện thực có phù hợp với các “thỏa thuận” đặc tả của chúng hay không.
- Jahob còn cho phép đặc tả các bất biến về các cấu trúc dữ liệu quan trọng cũng như các ràng buộc thiết kế.
- Chúng ta xét ví dụ về đặc tả của Jahob cho lớp List như được mô tả trong Hình 5..
- Trong ví dụ trên, đặc tả của lớp List sử dụng biến đặc tả content để chỉ tập các đối tượng thể hiện trong danh sách.
- Chương trình Jahob chỉ sử dụng nó cho mục đích đặc tả và bộ kiểm tra Jahob sử dụng nó để kiểm tra chương trình.
- Chi tiết về cấu trúc và cú pháp của ngôn ngữ đặc tả cho hệ thống Jahob chúng ta có thể tham khảo trong [22]..
- Hình 5: Minh họa đặc tả cho lớp List theo hệ thống Jahob.
- hỗ trợ đặc tả hình thức trong chương trình, cho phép khai báo các tiền và hậu điều kiện cho các thủ tục, các bất biến của kiểu dữ liệu.
- Hình 6 mô tả một ví dụ về đặc tả cho gói Stack bằng Ada 2012.
- Các hàm được đặc tả ngay sau phần khai báo và bắt đầu bằng từ khóa with.
- Hình 6: Minh họa đặc tả cho gói Stack bằng ngôn ngữ Ada 2012.
- 2.3 So sánh các ngôn ngữ đặc tả.
- Bảng 1 tổng kết và so sánh lại các ngôn ngữ đặc tả dựa trên một số các tiêu chí.
- Trong số các ngôn ngữ đặc tả theo phương pháp “thỏa thuận”.
- Hầu hết các ngôn ngữ trên đều bắt đầu từ ý tưởng nền tảng của JML, đây là ngôn ngữ tiên phong cho các ngôn ngữ đặc tả theo phương pháp.
- JML có ưu điểm là cấu trúc và cú pháp rõ ràng, đặc tả dựa trên ngôn ngữ chủ là ngôn ngữ Java đã trở nên rất phổ biến.
- Sự tách biệt giữa mã đặc tả và mã xử lý giúp cho hai công việc này hầu như tách biệt nhau.
- JML cho phép lồng ghép các đặc tả phi hình thức chung với các đặc tả hình thức nhằm hỗ trợ nhiều mức đặc tả cho chương trình..
- Đó là: thư viện API của ngôn ngữ Java đã được đặc.
- tả đầy đủ bằng ngôn ngữ JML.
- Do vậy, trong phần tiếp theo của bài báo này, JML là ngôn ngữ đặc tả.
- Bảng 1: So sánh các ngôn ngữ đặc tả hình thức theo hướng thoả thuận.
- Ngôn ngữ.
- Cách thức đặc tả.
- Các thành phần đặc tả.
- Kiểm tra tính đúng của phương thức được hiện thực so với đặc tả.
- Kiểm tra tính đúng của hàm được hiện thực so với đặc tả.
- Kiểm tra tính đúng của cấu trúc dữ liệu được hiện thực so với đặc tả.
- Kiểm tra tính đúng của hàm/ thủ tục được hiện thực so với đặc tả Hỗ trợ đặc.
- 3.1 Bộ đánh giá sự tương tự giữa các đặc tả Khối chức năng này giải quyết bài toán cơ bản để thực hiện việc tìm kiếm các đặc tả phù hợp với một yêu cầu đầu vào.
- Đó là đánh giá sự tương tự giữa các công thức logic đặc tả các hàm.
- Việc thu hẹp này dựa trên sự tính toán mức độ tương tự của đặc tả yêu cầu với các đặc tả của hàm API có trong thư viện..
- Gọi là một tập đặc tả được biểu diễn dưới dạng logic của các hàm thư viện.
- t m } là tập các mệnh đề (term) đặc tả trong .
- các đặc tả.
- đặc tả.
- Thư viện đặc tả hình thức cho các hàm Java API Đặc tả hình.
- Prototype trong ngôn ngữ Java.
- Hình 8: Một số đặc tả hàm bằng JML.
- Nhờ vào việc các hàm thư viện được đặc tả bằng các hàm logic và phương pháp tính độ tương tự giữa các đặc tả xây dựng được, chúng ta có thể phát triển một cơ chế tìm kiếm và tổng hợp các hàm API đáp ứng nhu cầu ban đầu dựa trên kỹ thuật lập kế hoạch trong lĩnh vực Trí tuệ Nhân tạo (AI Planning)..
- Với các hàm thư viện như mô tả trong Hình 8, giả sử chúng ta có một lời yêu cầu gọi hàm được đặc tả như sau:.
- Sử dụng cơ chế tính toán tương tự giữa các đặc tả như mô tả trong Phần 3.1, bộ lập kế hoạch xác định được hàm phù hợp nhất là f 3 .
- 3.3 Bộ tích hợp hàm mới vào thư viện đặc tả Chức năng này đóng vai trò giúp cho thư viện đặc tả các hàm của chúng ta phong phú thêm, giúp cho những lần sau khi gặp những yêu cầu tương tự, hệ thống sẽ có sẵn các hàm/ chuỗi các hàm đáp ứng yêu cầu, giúp tối ưu hiệu suất của hệ thống..
- Ví dụ, sau khi tìm ra lời giải tổng hợp cho yêu cầu được mô tả trong Phần 3.2, đặc tả và lời giải này lại được tiếp tục lưu trữ vào thư viện như một hàm mới (hàm f 4 ) để phục vụ cho những yêu cầu tìm kiếm và tổng hợp lời giải mới sau này..
- 4 MỘT SỐ BÀI TOÁN MINH HOẠ Sau đây là một số ví dụ minh họa việc sử dụng đặc tả JML để đặc tả cho các yêu cầu tìm kiếm và gọi hàm tự động từ một số trường hợp thực tế..
- Chúng ta đặc tả yêu cầu trên như sau:.
- 2 Để tính toán được rằng đặc tả của f 2 (x-x) là tương đương với đặc tả của subgoal, chúng ta sẽ cần đến một công cụ chứng minh (prover).
- Hàm pow() này có đặc tả JML như sau 3.
- Đặc tả JML cho yêu cầu:.
- Với phương pháp tương tự như yêu cầu 1, khung thức cũng dễ dàng tìm được 1 hàm thỏa mãn yêu cầu trên là hàm push() của lớp Stack, với đặc tả như sau:.
- Trường hợp 2: Cần tinh chế đặc tả mới có thể tìm ra lời gọi hàm..
- Đặc tả JML cho yêu cầu trên như sau:.
- 3 Đặc tả này đã có trong thư viện về đặc tả của các hàm thư viện của Java..
- Căn cứ vào hậu điều kiện của đặc tả yêu cầu trên, chúng ta sẽ tìm được hàm binarySearch() của lớp java.util.Arrays với đặc tả như sau:.
- Hàm sort() có đặc tả như sau:.
- Việc áp dụng ngôn ngữ đặc tả hình thức vào cơ chế tìm kiếm và tái sử dụng thành phần tự động là một hướng nghiên cứu mới, giúp cho kết quả tìm kiếm sẽ tốt hơn so với các nghiên cứu dựa trên từ khóa.
- Cho đến nay, các nghiên cứu về việc ứng dụng đặc tả hình thức, đặc biệt là với hướng tiếp cận thoả thuận, chỉ chủ yếu tập trung vào việc kiểm chứng tính đúng của phần mềm.
- chúng tôi đề xuất sử dụng các đặc tả hình thức vào việc tìm kiếm và tổng hợp các thành phần cần thiết theo nhu cầu của người lập trình.
- Từ đó, chúng tôi trình bày một khung thức để tìm kiếm và tổng hợp các API được mô tả bằng ngôn ngữ JML.
- Hiện tại, khung thức do chúng tôi đề nghị chủ yếu dựa trên đặc tả JML và sử dụng để tìm kiếm và tổng hợp các hàm API cho ngôn ngữ Java.
- Tuy nhiên, do bản chất của hình thức đặc tả trong khung thức là các công thức logic Hoare [16] nên khung thức này hoàn toàn có thể tuỳ biến hiệu quả để áp dụng cho các ngôn ngữ lập trình dạng câu lệnh (imperative) khác như C, C