Khóa luận Ứng dụng relational interface cho java - Đỗ Duy Hưng

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Đỗ Duy Hưng ỨNG DỤNG RELATIONAL INTERFACE CHO JAVA KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin Cán bộ hướng dẫn: Ths. Phạm Thị Kim Dung HÀ NỘI – 2010 Lời cảm ơn Trước tiên, tôi xin gửi lời cảm ơn và lòng biết ơn sâu sắc đến thạc sỹ Phạm Thị Kim Dung, người đã tận tình chỉ bảo hướng dẫn tôi trong suốt quá trình thực hiện khoá luận tốt nghiệp. Tôi xin bày tỏ lời cảm ơn sâu sắc đến các thầy cô giáo đã giảng dạy tôi trong suốt bốn năm học qua, đã cho tôi nhiều kiến thức quý báu để tôi vững bước trên con đường học tập của mình. Tôi xin gửi lời cảm ơn tới các bạn trong lớp K51CB, và K51CNPM đã ủng hộ khuyến khích tôi trong suốt quá trình học tập tại trường. Và cuối cùng, tôi xin bày tỏ niềm biết ơn vô hạn tới bố mẹ, và những người bạn thân luôn bên cạnh, động viên tôi trong suốt quá trình thực hiện khoá luận tốt nghiệp. Hà Nội, ngày 22 tháng 05 năm 2010 Sinh Viên Đỗ Duy Hưng TÓM TẮT NỘI DUNG Hiện nay, thiết kế dựa trên thành phần (Component-based design) đang được ứng dụng và phát triền mạnh vì những lợi ích mà nó mang lại cho ngành công nghệ phần mềm. Thiết kế dựa trên thành phần giúp cho việc xây dựng các hệ thống phức tạp, như là hệ thống nhúng, hệ thống vật lý trở nên hiệu quả và đáng tin cậy. Với kích cỡ và độ phức tạp lớn của hệ thống này không cho phép thiết kế toàn bộ từ đầu, hoặc xây dựng nó như là một đơn vị đơn lẻ. Thay vào đó, hệ thống phải được thiết kế như là một tập hợp các thành phần, một số được xây dựng từ đầu, một số kế thừa lại. Giao diện (Interface) đóng một vai trò quan trọng trong thiết kế dựa trên thành phần vì chúng cung cấp phương tiện để mô tả cho thành phần. Một interface có thể được xem như là một bản tóm tắt, một đại diện của thành phần: giữ lại các thông tin cần thiết của thành phần, giấu thông tin không cần thiết và làm cho mô tả thành phần trở nên đơn giản và hiệu quả hơn. Trong khóa luận tốt nghiệp này, bằng việc sử dụng lý thuyết về relational interface, tôi xây dựng một công cụ tự động phân tích, trích rút các thành phần có trong file mã nguồn Java và biến đổi nó thành các relational interface, thực hiện việc kết hợp tự động các interface này với nhau. Để từ đó, ta có thể biết được khả năng kết hợp của các thành phần này với nhau. Interface mới được kết hợp vẫn giữ nguyên tính chất của các interface cũ. Qua đó, ta cũng có thể dự đoán được giá trị đầu ra của các thành phần nếu biết được giá trị đầu vào thông qua các tính chất. MỤC LỤC Bảng các kí hiệu nghĩa tiếng anh Kí hiệu Diễn giải Input Đầu vào Output Đầu ra Well-formed Định dạng hoàn chỉnh Well-formable Định dạng có thể hoàn chỉnh Interface Giao diện Relational Interface Giao diện quan hệ Stateless Phi trạng thái Stateful Có trạng thái Feedback Phản hồi Formal methods Các phương pháp hình thức Formal specification Đặc tả hình thức Assumption Giả thiết Guarantee Bảo đảm Refinement Làm mịn Danh mục hình vẽ Hình 3.1: Sơ đồ một interface cho ví dụ 4 17 Hình 3.2: Sơ đồ một interface với feedback 19 Hình 4.1: Hàm parse() trong lớp JavaFile.java 32 Hình 4.2: Hàm parse() trong lớp JavaClass.java 33 Hình 4.3: Hàm Tools.rename(JavaMethod jm) 34 Hình 4.4: Hàm Tools. getRInterfaceList(JavaClass jc) 37 Hình 4.5: Hàm Shorten trong lớp Expression.java 39 Hình 5.1: Giao diện làm việc của Netbeans 41 Hình 5.2: Minh họa cách cài đặt thư viện (1) 42 Hình 5.3: Minh họa cách cài đặt thư viện (2) 42 Hình 5.4: Kết quả thử nghiệm 5.3.1 đối với hàm main 43 Hình 5.5: Kết quả thử nghiệm 5.3.1 đối với hàm cong 43 Hình 5.6: Kết quả thử nghiệm 5.3.1 đối với hàm tru 43 Hình 5.7: Kết quả thử nghiệm 5.3.1 đối với hàm nhan 44 Hình 5.8: Kết quả thử nghiệm 5.3.1 đối với hàm chia 44 Hình 5.9: Kết quả thử nghiệm 5.3.1 đối với hàm triTuyetDoi 44 Hình 5.10: Kết quả thử nghiệm 5.3.2 với hàm cong 45 Hình 5.11: Kết quả thử nghiệm 5.3.2 đối với hàm tru 45 Hình 5.12: Kết quả thử nghiệm 5.3.2 đối với hàm nhan 45 Hình 5.13: Kết quả thử nghiệm 5.3.2 đối với hàm chia 45 Hình 5.14: Kết quả thử nghiệm 5.3.2 đối với hàm triTuyetDoi 45 Hình 5.15: Biểu đồ interface cho kết hợp chia(cong(a, b), tru(a, b)) 46 Hình 5.16: Kết quả thử nghiệm 5.3.3 đối với hàm main 47 CHƯƠNG 1: MỞ ĐẦU Đặt vấn đề Hiện nay, với sự phát triển mạnh mẽ của công nghệ thông tin, nhiều hệ thống lớn được xây dựng nên nhằm mục đích giải quyết những bài toán với độ phức tạp tương đương. Với kích thước và độ phức tạp của những hệ thống như vậy, đòi hỏi phải có một phương pháp thiết kế hợp lý, hiệu quả và đáng tin cậy. Phương pháp thiết kế dựa trên thành phần đáp ứng được yêu cầu này, bởi vì, thay vì phải thiết kế toàn bộ từ đầu, hệ thống được thiết kế như là một tập các thành phần. Các thành phần này hoặc là được xây dựng lại từ đầu, hoặc là được thừa kế từ những thành phần khác. Do vậy mỗi thành phần phải có tính độc lập cao và chuẩn đặc tả rõ ràng. Điều này thường được thể hiện qua interface (giao diện) của thành phần. Một interface có thể coi như một đặc tả của một thành phần. Việc kết hợp các thành phần cũng thông qua việc kết hợp các interface. Nội dung bài toán Trong phương pháp thiết kế dựa trên thành phần, interface chính là đặc tả của thành phần, nên quá trình đặc tả interface là một trong những bước quan trọng, cần được quan tâm. Do vậy, trong khóa luận này tôi muốn đề cập đến phương pháp xây dựng interface cho mỗi thành phần một cách tự động. Hiện nay có rất nhiều lý thuyết về interface được đưa ra để mô tả thành phần. Tuy nhiên, các các interface này thường gặp phải một số khó khăn như không bắt được quan hệ giữa giá trị đầu vào và đầu ra, hay khó khăn trong việc kết hợp các interface với nhau. Để khắc phục những nhược điểm này, tôi đề xuất việc sử dụng relational interface trong đặc tả interface cho mỗi thành phần. Nhiệm vụ chính của bài toán là xây dựng công cụ chuyển đổi các thành phần có trong mã nguồn của ngôn ngữ lập trình hướng đối tượng thành relational interface, rồi kết hợp các interface này với nhau một cách tự động. Cấu trúc khóa luận Phần còn lại của khóa luận được cấu trúc như sau: Chương 2: Giới thiệu chung về kỹ nghệ hướng thành phần, phương pháp hình thức, đặc tả hình thức, đặc tả giao diện. Một số loại interface (giao diện) cùng với những ưu điểm, hạn chế của chúng. Giới thiệu chung về relational interface. Chương 3: Mô tả nội dung lý thuyết của relational interface, về môi trường và khả năng lắp ghép. Lý thuyết về kết hợp relational interfaces [7]. Chương 4: Áp dụng lý thuyết về relational interface và một số lý thuyết khác để xây dựng công cụ tự động chuyển đổi từ file mã nguồn Java sang relational interface. Chương 5: Thử nghiệm công cụ và đánh giá. Chương 6: Kết luận. CHƯƠNG 2: GIỚI THIỆU CHUNG VỀ ĐẶC TẢ VÀ GIAO DIỆN Công nghệ phần mềm hướng thành phần Công nghệ phần mềm hướng thành phần (component-based software engineering [8]) là một trong những bước tiến của quá trình sản xuất phần mềm trong công nghiệp. Nhờ vào đó, việc sản xuất phần mềm trở nên phát triển mạnh mẽ. Ta cùng nhìn lại các ngành kĩ nghệ khác. Mỗi ngành kĩ nghệ đều có riêng cho mình một số thành tố cơ bản. Sự khác biệt của công nghệ phần mềm so với các ngành kĩ nghệ khác là ở chỗ sự lắp ráp các thành phần khác nhau của phần mềm còn mang tính tùy biến. Nghĩa là đưa ra cùng hai linh kiện (hay thành phần) phần mềm với cùng một thiết kế, hai lập trình viên có thể lắp ráp theo cách khác nhau. Nhận thức được điều này, kỹ nghệ hướng thành phần trong sản xuất phần mềm được bắt đầu áp dụng. Điều cơ bản mà mỗi thành phần phải có là: tính độc lập cao và có chuẩn đặc tả rõ ràng cho từng thành. Đặc tả này phải không phụ thuộc vào cấu trúc bên trong của thành phần. Dựa trên 2 điểm cơ bản này của một thành phần, điều đầu tiên khi bắt đầu thiết kế thành phần là quan tâm đến đặc tả của thành phần. Điều này thường được thể hiện qua interface (giao diện). Tiếp theo, tính độc lập của thành phần. Do tất cả các thành phần được kết nối qua interface thay vì trực tiếp, mọi quá trình xây dựng bên trong thành phần đều được khép kín. Sự phụ thuộc sẽ chủ yếu dựa vào interface. Vì vậy sẽ tách được sự phụ thuộc về cách xây dựng bên trong. Việc xây dựng thành phần có thể bằng bất cứ phương pháp nào dù là lập trình cấu trúc hay lập trình hướng đối tượng. Đặc tả hình thức Phương pháp hình thức bao gồm một số các hoạt động khác nhau như: đặc tả hệ thống hình thức, dẫn chứng và phân tích đặc tả, phát triển chuyển đổi, và kiểm chứng chương trình. Tất cả các hoạt động này đều phụ thuộc vào đặc tả hình thức của phần mềm. Một đặc tả hình thức phần mềm là một đặc tả được thể hiện bằng một loại ngôn ngữ mà từ vựng, cú pháp, ngữ nghĩa của nó được định nghĩa một cách hình thức. Điều này có nghĩa là ngôn ngữ đặc tả phải được dựa trên các khái niệm toán học với thuộc tính đã được nghiên cứu và dễ hiểu [3]. Các phương pháp hình thức Trong tin học, thuật ngữ phương pháp hình thức [8] (ngôn ngữ hình thức, đặc tả hình thức,…) thường được dùng để chỉ các kỹ thuật dựa trên cơ sở toán học dùng trong quá trình mô tả chi tiết (đặc tả), phát triển và kiểm chứng các hệ thông phần mềm cũng như phần cứng. Cách tiếp cận này thường áp dụng cho các hệ thống có kết cầu chặt chẽ, đòi hỏi độ tin cậy và tính an toàn cao, để đảm bảo rằng trong quá trình xây dựng, phát triển hệ thống không xảy ra một lỗi nào, hoặc nếu có thì cũng là rất ít. Các phương pháp hình thức đặc biệt hiệu quả trong các giai đoạn đầu của quá trình xây dựng hệ thống (thường ở giai đoạn xác định yêu cầu và đặc tả hệ thống), tuy nhiên, chúng cũng có thể được dùng trong toàn bộ quy trình phát triển hệ thống. Các phương pháp hình thức có thể được xếp loại theo 3 mức độ như sau: Mức 0: Đặc tả hình thức được sử dụng để đặc tả hệ thống trước khi phát triển nó. Trong nhiều trường hợp thì việc sử dụng phương pháp hình thức ở giai đoạn này tỏ ra đặc biệt hiệu quả, nhất là về mặt chi phí. Mức 1: Phát triển và kiểm chứng hình thức có thể được áp dụng để tạo ra một chương trình (hay một hệ thống) một cách tự động, dựa trên các đặc tả hình thức đã có trước đó. Quá trình này đặc biệt thích hợp đối với các hệ thống đòi hỏi độ tin cậy và tính an toàn cao. Mức 2: Chứng minh tự động. Đặc tả Mô tả các cấu trúc, hoạt động của các sự vật hiện tượng, quá trình nào đó. Việc mô tả này có thể ở mức độ khái quát, nhưng cũng có thể là những mô tả ở mức độ hết sức chi tiết. Có nhiều ngôn ngữ cho phép đặc tả: Ngôn ngữ tự nhiên Ngôn ngữ toán Ngôn ngữ lập trình Ngôn ngữ hình thức Đặc tả hình thức Đặc tả hình thức là đặc tả với các tính chất: Chính xác và nhất quán. Ngắn gọn nhưng đầy đủ. Có thể xử lý bởi máy tính. Đặc tả hình thức có các ứng dụng như sau: Sử dụng trong giai đoạn phân tích, thiết kế, nhằm mục đích tạo ra các phác hoạ chi tiết, cụ thể và chặt chẽ về hệ thống sẽ được xây dựng. Trong quá trình xây dựng hệ thống, các đặc tả này sẽ là công cụ định hướng để đảm bảo hệ thống được xây dựng một cách phù hợp và đầy đủ. Sau khi hệ thống được xây dựng thì đặc tả sẽ đóng vai trò là thước đo để kiểm chúng, khẳng định hệ thống được tạo ra có đúng đắn và tin cậy hay không. Giao diện Đặc tả giao diện Các hệ thống lớn thường được chia thành các hệ thống nhỏ và các hệ thống nhỏ này được phát triển độc lập. Các hệ thống nhỏ tận dụng các hệ thống nhỏ khác, nên một phần quan trọng của quá trình đặc tả là định nghĩa những giao diện của hệ thống nhỏ. Ngay khi các giao diện được định nghĩa và chấp nhận, các hệ thống nhỏ có thể được phát triển độc lập. Giao diện của hệ thống nhỏ thường được định nghĩa như là một tập các đối tượng hoặc kiểu dữ liệu trừu tượng. Chúng mô tả dữ liệu và những hoạt động mà có thể được truy cập thông qua giao diện của các hệ thống nhỏ. Do đó, một đặc tả giao diện của hệ thống nhỏ có thể được tạo nên bằng cách kết hợp đặc tả của các thành phần được tạo nên bởi các giao diện hệ thống nhỏ [3]. Thành phần và giao diện Một cách chung mô tả cấu trúc của hệ thống là sơ đồ khối. Một sơ đồ khối bao gồm các thực thể gọi là các khối được kết nối với nhau bởi một liên kết. Cách mô tả này phân loại một cấu hình (mạng) cho truyền thông giữa các khối. Một khối có thể trình bày một thành phần vật lý hoặc logic, ví dụ như một phần của phần cứng hoặc phần mềm. Nhưng phổ biến hơn là nó trình bày một mô tả trừu tượng của thành phần hoặc một mô tả của interface thành phần. Mô tả thành phần trả lời cho câu hỏi: Nó làm gì ?does it do? Và một mô tả interface trả lời cho câu hỏi: nó được sử dụng như thế nào? Mô tả thành phần có thể rất gần với thành phần cơ bản, hoặc nó có thể chỉ định một vài thuộc tính đơn của thành phần cơ bản. Các mô tả của interface cũng có thể là chi tiết nhiều hoặc ít, nhưng chúng phải bao gồm đầy đủ thông tin để xác định các thành phần cơ sở được kết hợp và liên kết như thế nào. Và giống như bất kỳ việc trừu tượng hóa tốt nào, chúng không nên bao gồm nhiều thông tin. Các nhà thiết kế thành phần thường tạo nên các giả định về môi trường mà trong đó một thành phần có thể được triển khai [5]. Các loại interface Interface automata: có thể được sử dụng để bắt các mối quan hệ giữa input – output trong mô hình song song không đồng bộ và trong hầu hết các kiểu thực thi [4]. Relational nets: là một mạng của các tiến trình mà không xác định liên kết giữa giá trị input và giá trị output [5]. Assume/guarantee (A/G) interfaces: phân chia giữa giả thiết các giá trị đầu vào dựa trên các đảm bảo về giá trị đầu ra, nhưng interface này không bắt được mối quan hệ giữa các input và output [5]. Extended interfaces: giống với relational interface, tuy nhiên interface này không được đánh giá cao bởi hạn chế tính chất của những bước làm mịn và thực thi độc lập là không có[6]. Moore interfaces: được định nghĩa bởi công thức ϕi và ϕo. Trong đó công thức ϕi chỉ rõ giá trị hợp lệ của các biến input tại các trạng thái tiếp theo khi mà trạng thái hiện tại được cho trước, và công thức ϕo chỉ rõ giá trị hợp lệ của các biến output tại các trạng thái tiếp theo khi mà trạng thái hiện tại được cho trước. Công thức này không cho phép miêu tả mỗi quan hệ giữa input và output tại cùng một trạng thái [2]. Hạn chế của các interface trên là không bắt được mối quan hệ giữa input và output. Lý thuyết về relational interface giải quyết các vấn đề đó bằng việc xây dựng một thành phần ξ trong interface. ξ là tập tất các quan hệ giữa input và output, mô tả ràng buộc giữa input và môi trường. Việc kết hợp tổng quát các interfaces, có thể đạt được thông qua hai toán tử có tên là parallel conposition ( kết hợp song song ) và connection ( kết nối ) [5],[6]. Điều này cho phép tạo ra các feedback loop (phản hồi lặp) tùy ý. Khi nghiên cứu về relational interface, có rất nhiều vấn đề nảy sinh từ feekback loop đồng bộ. Có thể tránh vẫn đề được nảy sinh bởi feekback loop bằng cách hạn chế các trường hợp mà feedback loop được cho phép. Cụ thể, ta cho phép một output của một interface I được kết nối với một trong các input x của nó chỉ trong trường hợp I là Moore đối với x, có nghĩa ràng buộc của I không phụ thuộc vào x. Statelful và stateless interface [7] nói đến hai dạng của interface là stateless interface ( giao diện phi trạng thái ) và stateful interface ( giao diện có trạng thái ). Stateful interface, một ràng buộc có thể khác nhau tại mỗi trạng thái khác nhau. Stateless interface có thể được xem như một trường hợp đặc biệt của stateful interface khi ràng buộc là giống nhau ở tất cả các trạng thái. Trong trường hợp stateful, ta phân biệt giữa well-formed interface và well-formable interface (hai khái niệm này trùng khớp trong trường hợp stateless interface). Với well-formed interface, các ràng buộc luôn luôn được thỏa mãn tại mọi trạng thái có thể đạt được (reachable state). Well-formable interface không nhất thiết phải là well-formed, nhưng mà có thể được chuyển thành well-formed bằng cách hạn chế một cách hợp lý các input. Relational interface Trong khóa luận này, tôi muốn đề cập đến relational interface [7]. Relational interface là một interface chỉ ra những relation ( quan hệ ) giữa những input và output. Xem xét ví dụ về một thành phần đồng bộ sẽ lấy input là một số n ≥ 0 và trả về output là n + 1. Interface cho mỗi thành phần có thể được mô tả như là một quan hệ nhị phân giữa input và output: các relation chứa tất cả các cặp (n, n+1) với n ≥ 0. Mỗi một relation có thể được hiểu như một ràng buộc giữa thành phần và môi trường ( environment ) của nó: ràng buộc chỉ ra rằng với mỗi input hợp lệ, thoải mãn điều kiện mà môi trường cung cấp cho thành phần thì sẽ có nhưng output hợp lệ được tạo ra từ thành phần đó. Tính năng nổi trội của relational interface là ở việc giải quyết vấn đề bắt được quan hệ giữa input và output. Ngoài ra, lý thuyết về composition (kết hợp), connection (kết nối), feedback loop (phản hồi lặp) có trong relational interface có thể dẫn tới những khẳ năng: Thiết kế phần mềm dựa trên relational interface là sự kết hợp giữa các interface mà trong đó, các ràng buộc phải được thỏa mãn, hoặc có thể thỏa mãn. Ta cũng có thể kiểm chứng và dự đoán được khả năng kết hợp của các interface lại với nhau. Ngoài ra, dựa trên các rằng buộc, ta cũng có thể dự đoán được kết quả đầu ra từ dữ liệu đầu vào. Khả năng tối ưu hóa thiết kế phần mềm bằng tính chất refinement và shared-refinement. Một khái niệm quan trọng của relational interface mà đã được nhắc đến ở trên đó là well-formed và well-formable. Điều này giúp cho các thành phần, hay nói đúng hơn là các relational interface được liên kết hay có thể liên kết được với nhau. Với những định hướng này, và do giới hạn của khóa luận, tôi sẽ giải quyết vấn đề a, b, c. Vấn đề và những chế còn lại sẽ được giải quyết trong những nghiên cứu sau này. CHƯƠNG 3: NỘI DUNG LÝ THUYẾT VỀ RELATIONAL INTERFACE Tóm tắt về relational interface đã mô tả ở phần 2.3.5, trong chương này, tôi sẽ đề cập đến nội dung lý thuyết về relational interface. Nội dung lý thuyết này được sử dụng từ [7]. Sơ bộ về bài viết và các ký hiệu Trong bài viết này ta sử dụng first-order logic (FOL) như là một ngôn ngữ để mô tả ràng buộc. Ta sử dụng 2 hằng số logic đó là true và false. Các ký hiệu: ¬ : phép phủ định, ∧ : phép và, ∨ : phép hoặc, → : phép suy ra, ≡ : phép tương đương, ∀ : với mọi và ∃ : tồn tại. Chúng ta sử dụng kí hiệu ≔ để định nghĩa cho một khái niệm hoặc một kí hiệu mới, ví dụ: x0 ≔ max {1, 2, 3} chỉ ra rằng x0 là giá trị lớn nhất của tập {1, 2, 3} Gọi V là tập hữu hạn các biến. Một thuộc tính trên V là một công thức FOL ϕ như vậy thì với mọi biến tự do của ϕ đều thuộc V. Một tập tất cả các thuộc tính trên V được kí hiệu là ℱ(V). Coi ϕ là một thuộc tính trên V và V’ là tập con hữu hạn của V, V’ = {v1, v2, …, vn}. Khi đó, ∃V’ : ϕ là một cách viết ngắn gọn của ∃v1 : ∃v2 : … : ∃vn : ϕ. Tương tự như vậy, ∀V’ : ϕ là cách viết ngắn gọn của ∀v1 : ∀v2 : … : ∀vn : ϕ. Chúng ta hoàn toàn có thể giả định rằng tất cả các biến là kiểu, có nghĩa là tất cả các biến được kết hợp với một tập xác định nào đó. Một phép gán trên một tập các biến V là một hàm cho tướng ứng mỗi biến trong V với một giá trị nào trong tập xác định của biến đó. Một bộ các phép gán trên V được kí hiệu là 𝒜(V). Nếu a là một phép gán ( assignment ) trên V1 và b là một là một phép gán trên V2 ,và V1 và V2 là 2 tập tách rời thì chúng ta sẽ sử dụng (a, b) để kí hiệu một phép gán kết hợp trên V1 ∪ V2. Một công thức ϕ là thỏa mãn nếu ở đó tồn tại một phép gán a trên các biến tự do của ϕ để a thỏa mãn ϕ, được kí hiệu là a ⊨ ϕ. Một công thức ϕ là hợp lệ nếu nó được thỏa mãn bởi mọi phép gán. Nếu coi S là một tập hợp, S* là kí hiệu của tập hợp của tất cả các chuỗi hữu hạn được tạo nên bởi các phần tử trong S. S* bao gồm cả các chuỗi rỗng, kí hiệu là ε. Nếu s, s’ thuộc S* thì s ∙ s’ là phép nối của s và s’. |s| kí hiệu độ dài của s ∈ S*, với |ε| = 0 và |s ∙ a| = |s| + 1, với a ∈ S. Nếu s = a1a2…an, thì phần tử thứ i của chuỗi, ai, được kí hiệu là si, với i = 1, … , n. Relational interfaces Định nghĩa 1 (Relational interface): một relational interface (hay một interface đơn giản) là 1 bộ I = ( X, Y, ξ ). Trong đó X, Y là 2 tập hữu hạn và tách rời của các biến input và output tương ứng, và ξ là hàm tổng ξ: 𝒜(X ∪ Y)* → ℱ(X ∪ Y) Gọi 𝒜(V) là tập tất cả các phép gán trên tập các biến V. Do đó, 𝒜(X ∪ Y)* là tập tất cả các chuỗi hữu hạn của các phép gán trên X ∪ Y. Chú ý rằng X hoặc Y có thể là rỗng: nếu X là rỗng thì I là interface nguồn, nếu Y là rỗng thì I là một bộ chứa (sink). Một phần tử của 𝒜(X ∪ Y)* được gọi là một trạng thái (state). Trạng thái khởi tạo là một chuỗi rỗng ε. Gọi ℱ(X ∪ Y) là một tập tất cả các thuộc tính (property) trên X ∪ Y. Do đó, ξ liên kết với mỗi trạng thái s một công thức ξ(s) trên X ∪ Y. Công thức này thể hiện như là ràng buộc (contract) giữa I và môi trường của nó tại trạng thái đó. Khi ràng buộc thay đổi thì trạng thái của I thay đổi. Định nghĩa 2 (Assumption , Guarantees): Cho một ràng buộc ϕ ∈ ℱ(X ∪ Y), input assumptions của ϕ có công thức in(ϕ) ≔ ∃Y : ϕ. Output guarantees của ϕ có công thức out(ϕ) ≔ ∃X : ϕ. Chú ý rằng in(ϕ) là một thuộc tính trên X và out(ϕ) là một thuộc tính trên Y, và ϕ → in(ϕ), ϕ → out(ϕ) là công thức hợp lệ với mọi ϕ. Giả sử tại thời điểm ban đầu của một quy trình cho trước, trạng thái của I là s. Môi trường sẽ biểu diễn I với một phép gán aX trên biến input X, như vậy aX thỏa mãn giả thiết input in(ξ (s)). Sau đó, I sẽ chọn một phép gán aY trên biến output Y, để cả 2 phép gán đều thỏa mãn ξ(s). Những phép gán được kết hợp với nhau tạo ra 1 phép gán trên X ∪ Y, a ≔ (aX, aY). Tại thời điểm cuối của tiến trình, trạng thái mới của I là s ∙ a. Định nghĩa 3 (Stateless interface): Một interface I = (X, Y, ξ) là một interface phi trạng thái nếu với mọi s, s’ ∈ 𝒜(X ∪ Y)*, ξ(s) = ξ(s’). Trong interface phi trạng thái, ràng buộc độc lập với trạng thái. Với một interface phi trạng thái, ta có thể coi ξ như là một thuộc tính, thay vì một hàm ánh xạ các trạng thái tới các thuộc tính. Để rõ ràng hơn, ta sẽ biểu diễn I = (X, Y, ϕ) cho interface phi trạng thái, với ϕ là thuộc tính trên X ∪ Y. Ta cũng sẽ viết in(I) và out(I) thay cho in(ϕ) và out(ϕ). Ví dụ 1: Xem xét 1 thành phần với giả thiết input là một số dương n và trả về giá trị n hoặc n + 1 ở output. Chúng ta có thể biểu diễn thành phần này theo nhiều cách khác nhau. Một trong những cách biểu diễn theo interface phi trạng thái là: I1 ≔ ({x}, {y}, {x > 0 ∧ (y = x ∨ y = x + 1)}). Ở đây, x là biến input, và y là biến output. Ràng buộc của I1 là số dương x. Ta có in(I1) ≡ x > 0. Một interface phi trạng thái có thể khác của thành phần này là: I2 ≔ ({x}, {y}, { x > 0 → (y = x ∨ y = x + 1) }). Ràng buộc của I2 khác với của I1: nó cho phép x ≤ 0, nhưng nó không bảo đảm về output y trong trường hợp này. I2 được gọi là input-complete interface, trong trạng thái này nó chấp nhận tất cả các input. Ta có, in(I2) ≡ true. Nhìn chung, không gian trạng thái của một interface là vô hạn. Tuy nhiên trong một số trường hợp chỉ cần một tập hữu hạn các trạng thái để chỉ ra ξ. Ví dụ ξ có thể được chỉ ra bởi một máy tự động hữu hạn các trạng thái. Mọi trạng thái trong máy tự động được gán nhãn với một ràng buộc. Mọi bước chuyển tiếp (transition) của máy tự động được gán nhãn với một guard, hay nói cách khác, nó là một điều kiện trên các biến input và output. Những bước chuyển tiếp hướng ra ngoài của một trạng thái phải có các guard tách rời, và hợp của những guard phải là true. Một interface có thể được chỉ rõ như một máy tự động hữu hạn trạng thái được gọi là một interface hữu hạn trạng thái (finite-state interface). Các A/G interface là trường hợp đặc biệt của relational interface. Một A/G interface phi trạng thái là một bộ (X, Y, ϕx, ϕy), trong đó ϕx là một thuộc tính trên X biểu diễn giả thiết input và ϕy là một thuộc tính trên Y biểu diễn những bảo đảm output. Interface này có thể được biểu diễn đơn giản như là một relational interface (X, Y, ϕx ∧ ϕy). Định nghĩa 1 cho phép ràng buộc ξ(s) tại một trạng thái s nào đó trở thành một thuộc tính không thể thỏa mãn. Mặt khác, nhìn chung không phải tất cả các trạng thái có thể đạt được (reachable), vì không phải các input hoặc output là hợp lệ. Chúng ta có thể quan tâm đến các trạng thái với những ràng buộc không thể thỏa mãn khi mà các trạng thái này là có thể đạt được. Một “run” của I là một trạng thái s = a1...ak với k ≥ 0 (nếu k = 0 thì s = ε), để ∀i ∈ {1, …, k } : ai ⊨ ξ(a1…ai-1). Một trạng thái là có thể đạt được nếu nó là một “run”. Tập tất cả các trạng thái có thể đạt được của I được kí hiệu rồi ℛ(I), với mọi I. Định nghĩa 4 ( Well-formed interface ): Một interface I = (X, Y, ξ) được coi là well-formed nếu tất cả s ∈ ℛ(I), ξ(s) là có thể thể thoả mãn. Ví dụ 2: Đặt I ≔ ({x}, {y}, ξ), với x, y là kiểu boolean, và ξ(ε) ≔ true, ξ((x, _ ) ∙ s) ≔ false, ξ((¬x, _) ∙ s) ≔ true, với tất cả s. (x, _) chỉ ra bất cứ phép gán nào với x là true và (¬x, _) chỉ ra bất cứ phép gán nào với x là false. I không là well-formed, vì nó có những trạng thái có thể đạt được với ràng buộc là false ( tất cả các trạng thái bắt đầu với x là true). I có thể được chuyển đổi sang một well-formed interface bằng cách hạn chế ξ(ε) để tránh được những trạng thái có thể đạt được với những ràng buộc không thể thỏa mãn. Trong trường hợp cụ thể, đặt ξ(ε) ≔ ¬x, ta sẽ đạt được mục tiêu trên. Ví dụ 2 chỉ ra rằng một số interface mặc dù không là well-formed vẫn có thể được chuyển thành well-formed interface bằng cách hạn chế hợp lý các dữ liệu input. Định nghĩa 5 (Well-formable interface): một interface I = (X, Y, ξ) là well-formable nếu tồn tại một well-formed interface I’ = (X, Y, ξ’), như vậy: với tất cả s ∈ ℛ(I’), ξ’(s) ≡ ξ(s) ∧ ϕs, trong đó ϕs là một vài thuộc tính trên X. Rõ ràng, tất cả các well-formed interface là well-formable interface, nhưng điều ngược lại thì không đúng, như trong ví dụ 2 đã chỉ ra. Tuy nhiên, với interface phi trạng thái, 2 phép biều diễn này trùng nhau. Định lý 1: Một interface phi trạng thái I là well-formed nếu nó là well-formable. Định nghĩa 6 (Tương đương - Equivalence): 2 interface I = (X, Y, ξ) và I’ = (X’, Y’, ξ’) là tương đương, kí hiệu là I ≡ I’, nếu X = X’, Y = Y’, và với tất cả s ∈ ℛ(I) ∩ ℛ(I’), công thức ξ(s) ≡ ξ’(s) là hợp lệ. Bổ đề 1: Nếu I ≡ I’ thì ℛ(I) ≡ ℛ(I’) Môi trường và khả năng lắp ghép Định nghĩa 7 (Môi trường): Một interface là một bộ E = (X, Y, hX, hY), trong X và Y được định nghĩa trong Định nghĩa 1, và hX và hY là các hàm tổng. hX : 𝒜(X ∪ Y)* → ℱ(X), hY : 𝒜(X ∪ Y)* → ℱ(Y) hX biểu diễn những đảm bảo trên những input X, cái mà môi trường cung cấp tại những trạng thái cho trước, hY biểu diễn những đảm bảo mà môi trường kì vọng trên output Y. Các trạng thái được định nghĩa cho môi trường thì tương tự như là cho những interface. Một môi trường phi trạng thái (stateless environment) là môi trường mà hX(s) là và hY(s) là hằng số với tất cả các trạng thái s. Chúng ta định nghĩa tập hợp tất cả các trạng thái có thể đạt được của một môi trường E, kí hiệu là ℛ(E), theo cách tương tự như đối với interface: ε ∈ ℛ(E), và s ∙ a ∈ ℛ(E) nếu s ∈ ℛ(E) và a = (aX, aY) là một phép gán để aX ⊨ hX(s) và aY ⊨ hY(s). Một môi trường E được coi là “live” nếu với mọi s ∈ ℛ(E), cả hX(s) và hY(s) là có thể thỏa mãn. Định nghĩa 8 (Khả năng lắp ghép): Interface I = (X’, Y’, ξ) có thể ghép vào với môi trường E = (X, Y, hX, hY), được kí hiệu I ⊨ E, nếu X’ = X, Y’ = Y, và với tất cả s ∈ ℛ(IE), thì công thức sau là hợp lệ: hX(s) → (in(ξ(s)) ∧ (ξ(s) → hY(s))) (1) trong đó IE là một interface được định nghĩa như sau: IE ≔ (X, Y, ξE) (2) ξE(s) ≔ ξ(s) ∧ hX(s), với tất cả s ∈ 𝒜(X ∪ Y)* (3) Khả năng lắp ghép có thể được nhìn nhận một cách trực quan như là một trò chơi giữa interface và môi trường. Giả sử s là trạng thái hiện tại của I và E (ban đầu, s = ε). Nếu hX(s) không thỏa mãn thì E quyết định dừng cuộc chơi. Mặt khác, E chọn lựa một vài phép gán đầu vào ax thỏa mãn hX(s). Nếu ax vi phạm in(ξ(s)), thì điều kiện (1) sẽ bị vi phạm, và I sẽ không ghép được với E: và E sẽ bị “đổ lỗi” cho vi phạm này, điều này này sẽ cung cấp những bảo đảm không chắc chắn cho input. Mặt khác I chọn một phép gán đầu ra aY để phép gán đầu vào-đầu ra a ≔ (ax, ay) thỏa mãn ξ(s). Nếu aY vi phạm hY(s), thì điều kiện (1) sẽ bị vi phạm, một lần nữa điều này có nghĩa là I không thể ghép được với E: trong trường hợp này I bị “đổ lỗi”, vậy điều này cung cấp một bảo đảm không chắc chắn cho output. Mặt khác, một quy trình là hoàn thiện, và một trạng thái mới (cho cả I và E) là s ∙ a. Trò chơi tiếp tục với cách thức tương tự. Ví dụ 3: Xem xét interface phi trạng thái I1 và I2 từ ví dụ 1 và môi trường phi trạng thái E1 ≔ ({x}, {y}, x > 0, y > 0). Có thể thấy rằng cả I1 và I2 có thể lắp ghép với E2 ≔ ({x}, {y}, x ≥ 0, y > 0): ràng buộc x ≥ 0 không đủ mạnh để đạt giả thiết input x > 0. Cần chú ý rằng I2 không áp đặt giả thiết input một cách rõ ràng, tuy nhiên, nó lại ngầm sử dụng giả thiết này, vì nó không tạo nên bảo đảm nào khi giả thiết x > 0 bị vi phạm. Cuối cùng, xem xét E3 ≔ ({x}, {y}, true, true). I2 có thể ghép với E3: E3 không cung cấp bảo đảm trên input nhưng cũng không kì vọng bảo đảm trên output. I1 không thể ghép với E3 vì true x > 0. Interface IE được định nghĩa từ (2) và (3) có mục đích là chụp lấy trạng thái có thể đạt được của việc tổ hợp vòng lặp khép kín của E và I. Những trạng thái có thể đạt được này là tập con của các trạng thái có thể đạt được của I, bởi vì nhìn chung môi trường E chỉ có thể cung cấp một tập bị hạn chế các input, trong số tất cả các input hợp lệ với I. Hàm ràng buộc ξE của IE chụp được chính xác điều này. Bổ đề sau đây chỉ ra rằng trạng thái có thể đạt được của IE đúng là một tập con của các trạng thái có thể đạt được của I. Bổ đề 2: Cho I là một interface, E là một môi trường, và IE được định nghĩa như trong định nghĩa 8. Khi đó ℛ(IE) ⊆ ℛ(I). Bổ đề 3: Cho I, I’ là 2 interface, E là một môi trường và IE, I’E được định nghĩa như trong định nghĩa 8. Nếu I ≡ I’ thì ℛ(IE) = ℛ(I’E). Định lý 2: Nếu một interface I là well-formable thì tồn tại một môi trường thực (live environment) E để I ⊨ E. Vì well-formed có hàm ý là well-formable, nên hệ quả của định lý 2 là mọi interface là well-formed có thể được ghép với một vài môi trường thực. Chú ý rằng tồn tại những interface không là well-formed tuy nhiên lại có thể ghép được với những môi trường thực: những môi trường thực này hạn chế input, nên không bao giờ đạt được các trạng thái với những ràng buộc không thể thỏa mãn. Cũng tồn tại những interface là non-well-formed được mà có thể ghép được với những môi trường không thực (non-live environment): những môi trường này “dừng lại” sau một vài điểm, tức là, để hX(s) ≡ false với một vài trạng thái s. Cuối cùng, tồn tại các interface phi trạng thái và là non-well-formed. Các interface này có thể được ghép vào các môi trường không thực ít quan trọng mà dừng ngay lập tức. Định nghĩa 9 (Môi trường W.R.T tương đương): 2 interface I và I’ là 2 môi trường w.r.t tương đương, kí hiệu là I ≡E I’, nếu với bất kì môi trường E nào, I có thể ghép được với E nếu I’ có thể ghép được với E. Định lý 3: Với bất kì interface I, I’, I ≡ I’ nếu I ≡E I’. Kết hợp Chúng ta định nghĩa 2 dạng của việc kết hợp (Composition). Thứ nhất, chúng ta có thể kết hợp 2 interface I1 và I2 bằng cách kết nối một vài các biến ra vào của I1 với một vài các biến input của I2. Một output có thể được kết nối với một vài input, nhưng một input có thể được kết nối với nhiều nhất một output. Những kết nối sẽ tạo ra một interface phi trạng thái mới. Sau đó, quá trình kết hợp có thể được lặp lại để tạo nên những sơ đồ interface tùy ý. Việc kết hợp bằng kết nối mang tính liên kết, do đó thứ tự mà các interface được kết hợp là không quan trọng. 2 interface I = (X, Y, ξ) và I’ = (X’, Y’, ξ’) được gọi là tách rời nếu chúng có tập biến input và output tách rời nhau: (X ∪ Y) ∩ (X’ ∪ Y’) = ∅. Định nghĩa 10 (Kết hợp bằng kết nối): Đặt Ii = (Xi, Yi, ξi), với i = 1, 2 là là interface tách rời. Một kết nối θ giữa I1, I2 là một tập hữu hạn các cặp biến, θ = {(yi, xi) | i = 1, …, m}, như vậy: (1) ∀(y, x) ∈ θ : y ∈ Y1 ∧ x ∈ X2, và (2) ∀(y, x), (y’, x’) ∈ θ : x = x’ → y = y’. Các biến input và output bên ngoài là một tập hợp các biến Xθ(I1, I2) và Yθ(I1, I2) được lần lượt định nghĩa như sau ( với Xθ ≔ {x | ∃(y, x) ∈ θ} ): Xθ(I1, I2) ≔ (X1 ∪ X2) \ Xθ Yθ(I1, I2) ≔ Y1 ∪ Y2 ∪ Xθ Kết nối θ định nghĩa một interface tổ hợp θ(I1, I2) ≔ (Xθ(I1, I2) , Yθ(I1, I2), ξ), trong đó với mọi s ∈ 𝒜(Xθ(I1, I2) ∪ Yθ(I1, I2))*. ξ(s) ≔ ξ1(s1) ∧ ξ2(s2) ∧ ρθ ∧ ∀ Yθ(I1, I2) : Φ Φ ≔ (ξ1(s1) ∧ ρθ) → in(ξ2(s2)) (4) Và với i = 1, 2, si được định nghĩa là phép chiếu từ s tới các biến trong Xi ∪ Yi . Chú ý rằng, trong cách định nghĩa θ, Xθ ⊆ X2. Điều này hàm ý rằng X1 ⊆ Xθ(I1, I2), tức là mọi biến input của I1 cũng là mọi biến input của θ(I1, I2). Một kết nối θ được phép rỗng. Trong trường hợp này ρθ ≡ true. Và việc kết hợp này có thể được xem như là một kết hợp song song của 2 interface. Nếu θ là rỗng, thì ta viết I1 || I2 thay vì viết θ(I1, I2). Ta có thể kì vọng ràng buộc của việc kết hợp song song tại một trạng thái toàn cục cho trước là một phép hợp của các ràng buộc gốc tại trạng thái cục bộ tương ứng, điều này hàm ý rằng việc kết hợp song song có tính giao hoán. Bổ đề 4: Xem xét 2 interface tách rời Ii = (Xi, Yi, ξi), i = 1, 2. Khi đó I1 || I2 = (X1 ∪ X2, Y1 ∪ Y2, ξ), trong đó ξ thỏa mãn với tất cả s ∈ 𝒜(X1 ∪ X2 ∪ Y1 ∪ Y2)*, thì ξ(s) = ξ1(s1) ∧ ξ2(s2), với i = 1, 2, si phép chiếu từ s tới Xi ∪ Yi Định lý 4 (Kết hợp song song có tính giao hoán): cho 2 interface tách rời I1 và I2, I1 || I2 ≡ I2 || I1. Định lý 5 (Kết nối có tính liên kết): Cho I1, I2, I3 là những interface. Cho θ12 là một kết nối giữa I1 và I2, θ13 là một kết nối giữa I1 và I3, và θ23 là một kết nối giữa I2 và I3. Như vậy: (θ12 ∪ θ23) (I1, θ23(I2, I3)) ≡ (θ13 ∪ θ23) (θ12(I1, I2), I3) Hình 3.1: Sơ đồ một interface cho ví dụ 4 Ví dụ 4: Xem xét sơ đồ của interface phi trạng thái trong hình 1, với: Iid ≔ ({x1}, {y1}, y1 = x1) I+1 ≔ ({x2}, {y2}, y2 = x2 + 1) Ieq ≔ ({z1, z2}, {}, z1 = z2) Sơ đồ này có thể được xem như là phép kết hợp tương đương: θ2(I+1, θ1(Iid, Ieq)) ≡ (θ1 ∪ θ2)((Iid || I+1), Ieq) với θ1 ≔ {(y1, z1)} và θ2 ≔ {(y2, z2)}. Ta tiến hành hành tính toán ràng buộc của interface định rõ bởi sơ đồ. Cách làm này giúp cho việc xem xét kết hợp (θ1 ∪ θ2)((Iid || I+1), Ieq) dễ dàng hơn. Định nghĩa θ3 ≔ θ1 ∪ θ2. Từ bổ đề 4 ta có: Iid || I+1 = ({x1, x2}, {y1, y2}, y1 = x1 ∧ y2 = x2 + 1) Do đó, với θ3((Iid || I+1), Ieq), công thức (4) cho ta: Φ ≔ (y1 = x1 ∧ y2 = x2 + 1 ∧ y1 = z1 ∧ y2 = z2) → z1 = z2 Bằng việc loại bỏ các phép lượng hóa, ta có: ∀ y1, y2, z1, z2 : Φ ≡ x1 = x2 + 1 Do đó: θ3((Iid || I+1), Ieq) = ({x1, x2}, {y1, y2, z1, z2}, y1 = x1 ∧ y2 = x2 + 1 ∧ z1 = z2 ∧ y1 = z1 ∧ y2 = z2 ∧ x1 = x2 + 1) Chú ý rằng in(θ3((Iid || I+1), Ieq)) ≡ x1 = x2 + 1. Đó là, với liên kết θ, một giả thiết mới về input bên ngoài x1, x2 được tạo nên. Một interface tổ hợp không được bảo đảm là well-formed, thậm chí nếu các thành phần của nó là well-formed: Ví dụ 5: Xem xét phép kết hợp θ3((Iid || I+1), Ieq) được nói đến trong ví dụ 4, cho Iy là một interface phi trạng thái được định nghĩa như sau: Iy ≔ ({}, {y}, true) Cho θ4 ≔ {(y, x1), (y, x2)}. Có nghĩa là output y của Iy được kết nối tới cả output bên ngoài x1 và x2 của θ3((Iid || I+1), Ieq). Interface tổ hợp I4 ≔ θ4(Iy, θ3((Iid || I+1), Ieq)) không là well-formed, thậm chí cả hai Iy và θ3((Iid || I+1), Ieq) là well-formed. Đó là bởi vì, với I4, Công thức (4) cho ta: Φ ≔ (true ∧ y = x1 ∧ y = x2) → x1 = x2 + 1 Do đó: ∀ x1, x2, y1, y2, z1, z2 : Φ ≡ y = y + 1 Bởi vì công thức trên là không hợp lệ, nên I4 không là well-formed. Chú ý rằng tất các các interface trong ví dụ 5 là những interface phi trạng thái. Vì interface phi trạng thái, nên well-formedness và well-formability là trùng khớp, nên ví dụ 5 chỉ ra rằng kết nối là không thể duy trì được well-formability: I4 là không là well-formable, ngay cả khi cả Iy và θ3((Iid || I+1), Ieq) là well-formed. Các liên kết này có thể chụp được kết hợp nối tiếp nhưng không thể chụp được feekback ( phản hồi ). Để chụp được feekback, ta định nghĩa một loại thứ 2 của kết hợp, gọi là kết hợp phản hồi (feedback composition). Trong loại kết hợp này, một biến output của một interface I được kết nối với một trong các biến input x của nó. Với feekback, I yêu cầu phải là Moore đối với x. Một interface là Moore đối với một biến input cho trước x có nghĩa là ràng buộc này có thể phụ thuộc vào trạng thái hiện tại và phụ thuộc vào các biến input khác hơn là phụ thuộc vào x. Nó cho phép kết nối một output tới x để hình thành một feekback loop mà không tạo nên các vòng nhân quả. Định nghĩa 11 (Moore interface): Một interface I = (X, Y, ξ) là Moore đối với x ∈ X nếu với tất cả các s ∈ ℛ(I), ξ(s) là một thuộc tính trên (X ∪ Y) \ {x}. I là Moore khi nó là Moore đối với mọi x ∈ X. Định nghĩa 12 (Kết hợp bằng feedback): Cho I = (X, Y, ξ) là một Moore interface đối với một vài cổng vào x ∈ X. Một kết nối feekback κ trên I là một cặp (y, x), để y ∈ Y. Định nghĩa ρκ ≔ (x = y). Kết nối phản hồi κ định nghĩa interface sau: κ(I) ≔ (X \ {x}, Y ∪ {x}, ξκ) (5) ξκ(s) ≔ ξ(s) ∧ ρκ, với tất cả s ∈ 𝒜(X ∪ Y)* (6) Định lý 6 (Feedback có tính giao hoán): Cho I = (X, Y, ξ) là Moore interface đối với cả x1, x2 ∈ X, trong đó x1 ≠ x2. Cho κ1 = (y1, x1), và κ2 = (y2, x2) là các kết nối phản hồi. Khi đó κ1(κ2(I)) ≡ κ2(κ1(I)). Hình 3.2: Sơ đồ một interface với feedback Ví dụ 7: Xem xét sơ đồ của các interface trong hình 2. Giả sử IM là một Moore interface đối với u. Sơ đồ này có thể được diễn giải như là phép kết hợp κ ( θ ( I1, (I2 || IM)) ) Trong đó: θ ≔ {(y1, z1), (y2, x2)} và κ ≔ (w, u). Bổ đề 5: Cho I là một Moore interface đối với một vài biến input của nó, và cho κ là một kết nối feedback trên I. Khi đó ℛ(κ(I)) ⊆ ℛ(I). Bổ đề 6: Cho I = (X, Y, ξ) là một Moore interface đối với x ∈ X, và κ = (y, x) là kết nối feedback trên I. Cho κ(I) = (X \ {x}, Y ∪ {y}, ξκ) Khi đó với với bất kì s ∈ ℛ(κ(I)), công thức in(ξκ(s)) ≡ in(ξ(s)) là hợp lệ. Định lý 7 (Feedback duy trì well-formed): Cho I là một Moore interface đối với một vài biến input của nó, và cho κ là một kết nối feedback trên I. Nếu I là well-formed thì κ(I) là well-formed. Feedback không duy trì khả năng well-formed: Ví dụ 8: Xem xét một interface hữu hạn trạng thái If với 2 trạng thái, s0 (trạng thái ban đầu) và s1, một biến input x và một biến output y. If duy trì tại trạng thái s0 khi x ≠ 0 và chuyển từ trạng thái s0 sang trạng thái s1 khi x = 0. Cho ϕ0 ≔ y = 0 là ràng buộc tại trạng thái s0 và cho ϕ1 ≔ false là ràng buộc tại trạng thái s1. If không là well-formed bởi vì ϕ1 là không thỏa mãn, trong khi trạng thái s1 có thể đạt được. If là well-formable, tuy nhiên: If đủ để giới hạn ϕ0 thành ϕ’0 ≔ y = 0 ∧ x ≠ 0. Ký hiệu interface kết quả (là well-formed) là I’f . Cần chú ý If là Moore đối với x, trong khi I’f không là Moore với x. Cho κ là một kết nối feedback (y, x). Vì If là Moore, κ(If) được định nghĩa, và ràng buộc của nó tại trạng thái s0 là y = 0 ∧ x = y, và ràng buộc của nó tại trạng thái s1 là false ∧ x = y ≡ false. κ(If) không là well-formable: quả thực y = 0 ∧ x = y hàm ý x = 0, do đó trạng thái s1 là không thể tránh khỏi. CHƯƠNG 4: XÂY DỰNG CÔNG CỤ CHUYỂN ĐỔI TỰ ĐỘNG TỪ JAVA SANG RELATIONAL INTERFACE Cở sở lý thuyết Với lý thuyết về đặc tả hình thức interface cho phép thiết kế phần mềm dựa trên việc kết hợp giữa các interface, và mỗi interface là đại diện cho một thành phần. Trong chương này, tôi đưa ra mô hình thiết kế phần mềm dựa trên các interface. Các thành phần của lớp trong ngôn ngữ lập trình hướng đối tượng Hiện nay các ngôn ngữ lập trình hướng đối tượng phổ biến nhất đều tập trung theo phương pháp phân lớp (class) trong đó có C++, Java, C# và Visual Basic.NET. Một lớp có thể được hiểu là khuôn mẫu để tạo ra các đối tượng. Trong một lớp, người ta thường dùng các biến để mô tả các thuộc tính và các hàm để mô tả các phương thức của đối tượng. Khi đã định nghĩa được lớp, ta có thể tạo ra các đối tượng từ lớp này. Để việc sử dụng được dễ dàng, thông qua hệ thống hàm tạo (constructor), người ta dùng lớp như một kiểu dữ liệu để tạo ra các đối tượng. Phương thức (method ) của một lớp thường được dùng để mô tả các hành vi của đối tượng (hoặc của lớp). Ví dụ như đối tượng thuộc lớp điện thoại có các hành vi sau: Đổ chuông, chuyển tín hiệu từ sóng sang dạng nghe được, chuyển tín hiệu giọng nói sang dạng chuẩn, chuyển tín hiệu lên tổng đài.v.v. Khi thiết kế, người ta có thể dùng các phương thức để mô tả và thực hiện các hành vi của đối tượng. Mỗi phương thức thường được định nghĩa là một hàm, các thao tác để thực hiện hành vi đó được viết tại nội dung của hàm. Khi thực hiện hành vi này, đối tượng có thể phải thực hiện các hành vi khác. Ví dụ như điện thoại phải chuyển tín hiệu giọng nói sang dạng chuẩn trước khi chuyển lên tổng đài. Cho nên một phương thức trong một lớp có thể sử dụng phương thức khác trong quá trình thực hiện hành vi của mình. Thuộc tính (attribute) của một lớp bao gồm các biến, các hằng, hay tham số nội tại của lớp đó. Ở đây, vai trò quan trọng nhất của các thuộc tính là các biến vì chúng sẽ có thể bị thay đổi trong suốt quá trình hoạt động của một đối tượng. Các thuộc tính có thể được xác định kiểu và kiểu của chúng có thể là các kiểu dữ liệu cổ điển hay đó là một lớp đã định nghĩa từ trước. Như đã nói ở trên, trong mỗi một phương thức hay một lớp của ngôn ngữ lập trình hướng đối tượng, ta có thể coi nó như là một thành phần. Một thành phần có thể được tạo lập bằng một tập hợp của các thành phần con. Từ một thành phần (phương thức, lớp) ta có thể trích rút các input – các tham số, các quan hệ và các output chính là các giá trị trả về. Như vậy, với mỗi một phương thức ta có thể có một relational interface đại diện cho nó. Việc kết hợp các phương thức (ví dụ như việc gọi các phương thức lồng nhau) với nhau trong bài toán thực chính là việc tổ hợp các relational interface của các phương thức đó. Việc này sẽ giúp ta có một cái nhìn tổng quan về các ràng buộc của các phương thức sau khi kết hợp. Từ đó, với mỗi input, ta có thể dự đoán được output một cách đơn giản và hiệu quả thông qua các ràng buộc. Relational interface Lý thuyết được tôi sử dụng là toàn bộ lý thuyết về relational interface được nêu lên ở chương 2, nhưng lý thuyết chính để xây dựng công cụ này là về relational interface và kết hợp relational interface, được nêu ra trong phần 3.2 và 3.4. Phần 3.2 chỉ ra rằng, một relational interface là một bộ I = ( X, Y, ξ ). Trong đó X, Y là 2 tập hữu hạn và tách rời của các biến input và output tương ứng, và ξ là hàm tổng ξ: 𝒜(X ∪ Y)* → ℱ(X ∪ Y) ξ là một biểu thức ánh xạ từ tập các chuỗi hữu hạn các phép gán đến tập tính chất trên tập X ∪ Y. Điều này có nghĩa là ξ biểu diễn được mối quan hệ giữa input và output mà vẫn thỏa mãn được tính chất trên toàn tập X ∪ Y. Phần 3.4 chỉ ra cách thức kết hợp 2 relational interface I1 và I2 với nhau. Có 2 kiểu kết hợp được nêu ra ở đây: kết hợp bằng kết nối (Composition by connection) được nêu ra ở định nghĩa 10, và kết hợp bằng phản hồi lặp (Composition by feedback loop) được nêu ra ở định nghĩa 12. Bằng việc kết hợp này một interface mới được tạo ra mà ràng buộc về tính chất của 2 interface I1 và I2 vẫn được giữ. Với một hàm tổng ξ mới, mối quan hệ giữa input và output mà vẫn thỏa mãn được tính chất trên toàn tập X(I1, I2) ∪ Y(I1, I2). Từ định nghĩa 4 và 5, tính chất well-formed và well-formable chỉ ra rằng ràng buộc ξ được thỏa mãn hay có thể được thỏa mãn. Điều này có nghĩa là một relational interface với ràng buộc không thỏa mãn thì không tìm được output. Và một relational interface với ràng buộc có thể được thỏa mãn được phép hạn chế tính chất đầu vào để thu được ràng buộc được thỏa mãn, tức là tìm được output. Khi kết hợp, một relational interface mới và một ràng buộc ξ mới được tạo ra. Nếu ràng buộc ξ mới này là được thỏa mãn thì 2 interface có thể kết hợp với nhau mà vẫn thu được output. Một số kiến thức về logic Trong khóa luận này, tôi sử dụng một số kiến thức logic dưới đây [1] để phục vụ cho việc tính toán các ràng buộc trong interface. Tuyển sơ cấp và hội sơ cấp Ký hiệu: ¬A là phủ định của A. Tuyển sơ cấp là tuyển của các biến mệnh đề X, Y, Z, ¬X, ¬Y, ¬Z (có thể có cả chỉ số nữa) Hội sơ cấp là hội của các biến mệnh đề X, Y, Z, ¬X, ¬Y, ¬Z ( có thể có cả chỉ số nữa ) Dạng chuẩn tắc hội và dạng chuẩn tắc tuyển của công thức Dạng chuẩn tắc hội (DCTH) là hội của các tuyển sơ cấp (TSC), hay: DCTH ≡ (TSC)1 ∧ (TSC)2 ∧ … ∧ (TSC)n (n ≥ 1). Dạng chuẩn tắc tuyển (DCTT) là tuyển của các hội sơ cấp (HSC), hay: DCTT ≡ (HSC)1 ∧ (HSC)2 ∧ … ∧ (HSC)m (m ≥ 1). Các công thức đồng nhất bằng nhau (1) ¬(¬A) ≡ A (luật phủ định kép). (2) A ∨ B ≡ B ∨ A (luật giao hoán đối với các phép tuyển). (3) A ∧ B ≡ B ∧ A (luật giao hoán đối với các phép hội). (4) (A ∨ B) ∨ C ≡ A ∨ (B ∨ C) ≡ A ∨ B ∨ C (luật kết hợp đối với phép tuyển). (5) (A ∧ B) ∧ C ≡ A ∧ (B ∧ C) ≡ A ∧ B ∧ C (luật kết hợp đối với phép hội) (6) ¬(A ∨ B) ≡ ¬A ∧ ¬B (luật De Morgan đối với phép tuyển) (7) ¬(A ∧ B) ≡ ¬A ∨ ¬B (luật De Morgan đối với phép hội) (8) A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C) (luật phân bố giữa phép tuyển đối với phép hội). (9) A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C) (luật phân bố giữa phép hội đối với phép tuyển). (10) A ∨ (A ∧ B) ≡ A (luật hấp thụ giữa phép tuyển với phép hội). (11) A ∧ (A ∨ B) ≡ A (luật hấp thụ giữa phép hội với phép tuyển). (12) A → B ≡ ¬A ∨ B (luật khử phép kéo theo) (13) A ∨ A ≡ A (luật lũy đẳng đối với phép tuyển). (14) A ∧ A ≡ A (luật lũy đẳng đối với phép hội). (15) A ∨ 0 ≡ A (luật trung hòa đối với hằng sai). (16) A ∧ 1 ≡ A (luật trung hòa đối với hằng đúng). (17) A ∨ 1 ≡ 1 (luật thống trị đối với hằng đúng). (18) A ∧ 0 ≡ 0 (luật thống trị đối với hằng sai). (19) A ∨ ¬A ≡ 1 (luật phần tử bù đối với phép tuyển) (20) A ∧ ¬A ≡ 0 (luật phần tử bù đối với phép hội). Các công thức đồng nhất bằng nhau (1) đến (20) cho phép ta khẳng định một công thức A bất kì là hằng đúng hay hằng sai, hoặc thực hiện được hay không và nó được ứng dụng để tìm dạng chuẩn tắc hội, dạng chuẩn tắc tuyển. Mục tiêu của bài toán Sau khi nghiên cứu về relational interface, tôi nhận thấy rằng hoàn toàn có thể áp dụng được lý thuyết này cho những thành phần (phương thức, lớp) của một ngôn ngữ lập trình hướng đối tượng. Cụ thể, nếu mỗi một thành phần, có một interface đại diện cho nó, thì thông qua interface này biết được những ràng buộc, những quan hệ có trong thành phần. Ngoài ra, ta còn có thể biết được khả năng kết hợp, và các tính chất sau khi kết hợp giữa các thành phần thông qua việc kết hợp các interface là đại diện của chúng. Thông qua những interface này, ta còn có thể dự đoán được chính xác giá trị đầu ra của thành phần, nếu như biết trước giá trị đầu vào. Với những mong muốn trên, tôi xây dựng một công cụ tự động phân tích, chuyển đổi từ những phương thức có trong file mã nguồn của một ngôn ngữ lập trình hướng đối tượng thành những relational interface tương ứng. Sau đó tiến hành kết hợp các relational interface này theo thứ tự kết hợp các thành phần của chúng có trong hàm main, nếu như tồn tại việc kết hợp giữa các thành phần ở hàm main. Trong khóa luận này, tôi sử dụng ngôn ngữ lập trình Java để xây dựng một công cụ và cũng sử dụng file mã nguồn .java như là dữ liệu đầu vào. Nhấn mạnh rằng, việc phân tích dữ liệu đầu vào của file mã nguồn của các ngôn ngữ lập trình hướng đối tướng khác như C# cũng không khác nhiều. Điều nay phụ thuộc vào cấu trúc cú pháp của mỗi ngôn ngữ lập trình. Hướng giải quyết bài toán Tạo relational interface tự động từ phương thức Đầu tiên ta sẽ tiến hành phân tích nội dung của file java để tách ra được các lớp, các phương thức, và các thuộc tính của lớp. Việc tách nội dung file .java dựa trên cấu trúc ngữ pháp trong java. Như vậy nếu ta coi mỗi một phương thức của một lớp là một thành phần, thì ta hoàn toàn có thể đưa ra được relational interface đại diện cho thành phần này, với input là tập tham chiếu truyền vào, output là tập giá trị trả về, và ξ chính là nội dung của của phương thức. Ví dụ, với một phương thức cộng: public static float cong(float a, float b) { return a + b; } Dự liệu truyền vào là a và b, trả về là a + b, như vậy ta sẽ có relational interface đại diện cho phương thức này là I1 = ({x1, x2}, {y1}, y1 = x1 + x2). Phức tạp hơn, với những phương thức chứa cấu trúc điều khiển if… else như đối với một phương thức tính giá trị tuyệt đối sau: public static float triTuyetDoi(float a) { if (a >= 0) { return a; } else { return -a; } } Lúc này relational interface đại diện cho phương thức này có dạng: I2 = ({x}, {y}, x ≥ 0 ∧ y = x ∨ x < 0 ∧ y = -x). Do giới hạn của khóa luận, tôi mới chỉ thực hiện việc phân tích trên những phương thức có cấu trúc đơn giản như lấy giá trị trả về hoặc chứa câu lệnh điều khiển if…else… Tính input assumption tự động Một trong những vấn đề của bài toán là làm sao để tính được input assumption (giả thiết đầu vào) một cách tự động. Từ định nghĩa 2 (phần 3.2): Cho một ràng buộc ϕ ∈ ℱ(X ∪ Y), input assumption của ϕ có công thức in(ϕ) ≔ ∃Y : ϕ, và in(ϕ) là một thuộc tính trên X. Như vậy, ta sẽ tính in(ϕ) bằng cách giả sử ∃Y làm cho ϕ thỏa mãn hay ϕ ≔ true. Do ϕ là một công thức FOL, bằng cách cho những ràng buộc trên Y có giá trị là true, sau đó áp dụng luật trung hòa đối với hằng đúng và luật thống trị đối với hằng đúng (A ∧ 1 ≡ A, A ∨ 1 ≡ A). Ta sẽ có được in(ϕ). Ví dụ: Với interface I = ({x}, {y}, x > 0 ∧ (y = x ∨ y = x + 1)) Để tính in(I), ta coi y = x ≔ true và y = x + 1 ≔ true, khi đó in(I) ≔ x > 0 ∧ (true ∨ true) ≡ x > 0. Vậy in(I) ≔ x > 0. Tính ξ mới được tạo ra tự động Từ định nghĩa 10 (phần 3.4) ta có: ξ(s) ≔ ξ1(s1) ∧ ξ2(s2) ∧ ρθ ∧ ∀Yθ(I1, I2) : Φ Φ ≔ (ξ1(s1) ∧ ρθ) → in(ξ2(s2)) Do việc, tính toán ξ1(s1) ∧ ξ2(s2) ∧ ρθ khá là đơn giản, bài toán được đưa về việc tính: ∀Yθ(I1, I2) : Φ. Điều này có nghĩa là ta cần tìm quan hệ giữa các xi , xi ∈ Xθ(I1,I2) sao cho ∀Yθ(I1, I2) : Φ. Giải hệ các ràng buộc Φ sẽ có được các quan hệ cần tìm. Thực hiện việc kết hợp tự động Ta sẽ tiến hành phân tích hàm main để đưa ra thứ tự kết hợp các phương thức của lớp. Thứ tự các kết hợp các interface đại diện cho các phương thức này chính là thứ tự kết hợp các phương thức có trong hàm main. public static void main(String[] args) throws Exception { float a = 2; float b = 3; float result; result = chia(cong(a, b), nhan(a, b)); } Bằng việc chuyển đổi những phương thức cong, nhan, và chia có trong lớp thành relational interface, ta có được 3 relational interface tương ứng là I+, I*, I/. Ở bước này, ta chưa cần quan tâm giá trị đầu vào của biến a, b là bao nhiêu. Việc cần làm là ta phải tiến hành kết hợp 3 interface I+, I*, I/ theo đúng thứ tự với chia(cong(a, b), nhan(a, b)). Việc kết hợp được bắt đầu tại những phương thức được sẽ được tính toán theo độ ưu tiên cao nhất. Ở đây, 2 phương thức cong và nhan sẽ được tính trước. Ứng với 2 phương thức này ta có 2 relational interface là I+, I* phép kết hợp giữa I+ và I* là song song bởi vì kết nối θ1 giữa I+ và I* là rỗng. Gọi θ2 là kết nối giữa I/ với I+ và I*. Như vậy, kết nối tổng hợp của 3 interface này là: θ2(I/, θ1(I+, I*)) ≡ (θ2 ∪ θ1)((I+ || I*), I/) Từ đây, ta sẽ tính ra được input, output và ξ của interface tổng hợp. Do vậy relational interface tổng hợp là hoàn toàn tính được. Tóm lại, với đầu vào là một file .java, ta đã đạt được mục tiêu là đưa ra được các relational interface đại diện cho mỗi phương thức và interface tổng hợp như mong muốn. Tuy rằng, công cụ này vẫn còn tồn tại một số những hạn chế như mới chỉ phân tích được những file mã nguồn có cấu trúc đơn giản, chưa thực hiện kết hợp interface bằng phản hồi (composition by feedback), …, nhưng những hạn chế này sẽ được tôi khắc phục trong những nghiên cứu sau này. Mô tả các thành phần của công cụ Thành phần của công cụ này bao gồm các package (gói) và các class (lớp) chính sau: [package] relational_interface RInterface.java [package] java_source SourceFormat.java JavaFile.java JavaClass.java Tools.java [package] first_order_logic Expresstion.java FOLOptimizer.java Ngoài ra còn có một số các lớp khác như : JavaAttribute.java: mô tả thuộc tính trong lớp, bao gồm mức độ truy cập ( public, protected, hoặc private ), tên thuộc tính, kiểu thuộc tính, và giá trị của thuộc tính đó. JavaMethod.java: mô tả các phương thức của lớp, bao gồm mức độ truy cập ( public, protected, hoặc private ), tên phương thức, giá trị trả về, danh sách tham số, và nội dung của phương thức. JavaParameter.java: mô tả tham số của phương thức, bao gồm kiểu và tên của tham số. Keyword: Phân loại và lưu trữ các từ khóa trong java, như từ khóa chỉ đối tượng gồm có interface, class. Từ khóa chỉ tính thừa kế gồm: extends, implements. Từ khóa chỉ mức độ truy cập: public, protected, private và một số loại từ khóa khác… Logic.java: mô tả các toán tử logic như AND (“&”), OR (“|”), NOT (“!”). Lớp SourceFormat.java Lớp SourceFormat.java cho phép ta có thể đọc những file.java và đưa chúng về một định dạng chuẩn. Hàm khởi tạo public SourceFormat(String str): với tham số truyền vào là tên file .java muốn xử lý. Hàm public void readFile(): để đọc nội dung các file được truyền vào và sinh ra ngoại lệ nếu như không tìm được file truyền vào. Hàm public void delComments(): Xóa đi các comment có trong file. Các comment trong file .java có định dạng là: /* */ hoặc comment cả dòng, // . Hàm public void makeSpaces(): Tạo ra các khoảng trắng tại 2 bên của các kí tự ( , ) , { , } , + , - , * , / , : , và , Hàm public String solveString(String s): Xử lý từng dòng được đọc vào ở hàm readFile(). Hàm public String returnString(): trả về nội dung code dưới dạng String trong file.java sau khi đã được chuẩn hóa. Lớp RInterface.java Lớp Rinterface.java lưu trữ cấu trúc dữ liệu của một relational interface. Bao gồm: tên của relational interface là String name, danh sách tên input dưới dạng ArrayList inputs, danh sách tên ouput dưới dạng ArrayList outputs. Quan hệ String relation ở dạng chuẩn tắc tuyển của tập các biến, mỗi biến này đại diện cho một biểu thức (ràng buộc). Ta sử dụng Hashtable để lưu trữ từng cặp tương ứng. Hàm khởi tạo RInterface(JavaMethod jm, int pos): Đây là hàm chính của lớp này. Với tham chiếu truyền vào là JavaMethod không phải là hàm main, hàm sẽ tạo ra một relational interface đại diện cho phương thức jm của lớp. Tham chiếu pos nói lên vị trí của phương thức jm trong lớp, điều này phục vụ cho việc đặt tên giá trị trả về. Do công cụ mới chỉ giải quyết được trên các phương thức với nội dung đơn giản cho nên thuật toán của hàm này như sau: Đầu tiên, hàm sẽ tiến hành việc kiểm tra xem JavaMethod jm có phải là hàm main không bằng cách so sánh tên của jm. Nếu đúng thì return, còn nếu sai thì thực hiện tiếp chương trình. Tên của relational interface tạo ra trùng với tên phương thức jm. Input của relational interface mới chính là các tham chiếu của jm. Tên của output được đặt là y + . (ví dụ y1, y2, …). Quan hệ chính là 1 biểu thức với vế trái là output, vế phải là biểu thức trả về, được ký hiệu là rx. Nếu như trong phương thức chứa câu lệnh điều khiển if…else hoặc if… thì mỗi một điều kiện của if hoặc else cũng được coi như là một quan hệ, được kí hiệu là rif, relse. Lúc này quan hệ trả về sẽ là rif ∧ rx1 ∨ relse ∧ rx2 nếu như câu lệnh điều khiển là if…else hoặc rif & rx1 nếu như câu lệnh điều khiển chỉ có if. Với rx1 và rx2 là quan hệ bên trong khối { } của if và else. Lớp JavaFile.java Lớp JavaFile.java cho phép ta đọc file .java và phân tích nội dung code của file này. Chuyển chúng về cấu trúc dữ liệu JavaClass. Hàm khởi tạo public JavaFile(String sourceFiles): Tham số truyền vào là tên của file. Sau đó chương trình sẽ tiến hành phân tích các từ tố (token), tách chúng thành từng lớp khác nhau và tiến hành xử lý trong các lớp. Các từ tố được lưu trữ dưới dạng một ArrayList. Hàm private void stringTokenizer(): Bằng việc sử dụng lớp StringTokenizer có trong Java, hàm nay sẽ tiến hành tách code của file java ( dưới dạng String ) thành một ArrayList tokens. Hàm private ArrayList parse(): Mục đích của hàm này là tìm các lớp có trong code của file .java. Từ mảng các từ tố, chương trình sẽ tìm những từ tố có giá trị là “Class” rồi từ đó phân tích tên, cũng như nội dung bên trong cặp { … } của lớp private ArrayList parse() { ArrayList _jcs = new ArrayList(); int pos = 0; while (pos < tokens.size()) { if (tokens.get(pos).equals(Keyword.CLASS)) { // } else { pos++; } } return _jcs; } Hình 3.1: Hàm parse() trong lớp JavaFile.java Lớp JavaClass.java Lớp JavaClass mô tả cấu trúc của một class trong java. Bao gồm tên, danh sách các thuộc tính, danh sách các phương thức có trong lớp. Một số hàm chính trong lớp: Hàm khởi tạo public JavaClass(): khởi tạo các giá trị thuộc tính. Hàm public void parse(): Sử dụng kiến thức về cấu trúc ngữ pháp trong java, hàm này có nhiệm vụ phân tích nội dung của class. Nội dung được phân tích là ArrayList contents. Để tách ra các thuộc tính hay các phương thức, ta đi từ những từ tố có giá trị là các mức độ truy cập như là: public, protected, private. Sau đó ta sẽ phân tích các từ tố tiếp theo để nhận biết ra đó là thuộc tính hay phương thức. Nếu một trong các từ tố tiếp theo có giá trị là “;” thì đó là thuộc tính, còn nếu có giá trị là “(” thì đó là phương thức. Ví dụ: khai báo một thuộc tính là private static final int x = 2; hoặc private int x; , còn khai báo một phương thức là: public int add (int a, int b) { } int pos = 0; int size = contents.size(); while (pos < size) { if (Keyword.isVisibilityKeyword(contents.get(pos))) { String visibility = contents.get(pos); boolean isMethod = true; for (int i = pos + 1; i < size; i++) { if (contents.get(i).equals(";")) { isMethod = false; break; } else if (contents.get(i).equals("(")) { break; } } if (isMethod) { // qua trinh xu ly neu la phuong thuc // … } else { // qua trinh xu ly neu la thuoc tinh // … } } pos++; } } Hình 4.2: Hàm parse() trong lớp JavaClass.java Tuy nhiên, hạn chế của cách làm này là dữ liệu đưa vào phải là được định dạng chuẩn, tức là phải có đầy đủ mức độ truy cập cho mỗi thuộc tính và phương thức. Ngoài ra còn hàm public void display() được sử dụng để hiển thị thông tin của mỗi class. Lớp Tools.java Đây là một trong những lớp quan trọng của công cụ, chứa những phương thức phục vụ cho việc giải quyết bài toán. Hai biến toàn cục public static int numOfRelation và public static int numOfInput được dùng để lưu số lượng quan hệ và input được tạo ra. Chủ yếu phục vụ cho việc đổi tên. Hàm public static void rename(JavaMethod jm): Để tránh việc bị trùng lặp tên input giữa các interface sau khi chuyển đổi từ JavaClass sang Releational Interface, hàm này được tạo nên để đổi tên các tham chiếu của các phương thức. Cách thức hoạt động của hàm này như sau: đầu tiên ứng với mỗi tham chiếu, ta sẽ có một tên mới. Quy tắc đặt tên mới là: ≔ “x” + . Sau đó các cặp và được lưu trữ trong Hashtable, với key là và value là . Tiếp đó, ta tiến hành đổi tên trong nội dung của các phương thức dựa vào Hashtable đã tạo. public static void rename(JavaMethod jm) { Hashtable name = new Hashtable(); // them ten, ten moi cua method vao hashtable ArrayList jp = jm.parameters; for (int j = 0; j < jp.size(); j++) { numOfInput++; String newName = "x" + String.valueOf(numOfInput); name.put(jp.get(j).name, newName); jp.get(j).setName(newName); } ArrayList contents = jm.contents; for (int j = 0; j < contents.size(); j++) { String str = contents.get(j); if (name.containsKey(str)) { contents.set(j, (String) name.get(str)); } } name.clear(); } Hình 4.3: Hàm Tools.rename(JavaMethod jm) Hàm public static RInterface parse (ArrayList arr, ArrayList ris): Hàm này được dùng để phân tích thứ tự kết hợp giữa các interface với tham chiếu truyền vào là công thức kết hợp dưới dạng ArrayList, và ArrayList. Hàm sẽ trả về relational interface đã được kết hợp. Ví dụ như truyền vào ArrayList là “cong ( tru ( a , b ) , nhan ( a , b ) )” với ris bao gồm các Rinterface là { cong, tru, nhan chia }. Thuật toán được sử dụng để phân tích chuỗi kết hợp này là như sau. Bước 1: Ta sẽ đánh mức độ ưu tiên tính toán cho mỗi thành phần (thành phần là tên của relational interface hoặc tên của tham chiếu trong ArrayList arr, bỏ qua: ‘(‘, ‘)’ và ‘,’). Độ ưu tiên của mỗi thành phần ≔ - . Đưa tất cả thành phần một danh sách, và đưa độ ưu tiên tương ứng của chúng vào một danh sách khác. Với ví dụ trên, ta sẽ có danh sách các thành phần arr1 = [cong, tru, a, b, nhan, a, b] , tương ứng mỗi thành phần ta có danh sách độ ưu tiên arr2 = [0, 1, 2, 2, 1, 2, 2]. Điều này có nghĩa là độ ưu tiên của cong là 0, độ ưu tiên của tru và nhan là 1, độ ưu tiên của a và b trong cả 2 lần xuất hiện là 2. Việc xử lý bài toán sẽ đi từ độ ưu tiên cao nhất. Gọi max là độ ưu tiên có giá trị lớn nhất. Như vậy, với danh sách trên thì ban đầu giá trị của max là 2. Bước 2: Ta tiến hành duyệt danh sách từ độ ưu tiên từ đầu tới cuối. Giả sử tại vị trí i của danh sách, giá trị của độ ưu tiên này là max-1, tại những vị trí tiếp theo: i+1, …i + n, độ ưu tiên đều có giá trị là max ( độ ưu tiên tại vị trí i+n+1 có giá trị khác max). Ứng với mỗi vị trí từ i đến i+n trong danh sách thành phần, ta có danh sách các Rinterface là ri, ri+1, … ri+n. Chú ý rằng ri sẽ là null nếu như thành phần ở vị trí i trong danh sách các thành phần là tham chiếu (không phải là interface). Sau đó ta tiến hành kết hợp các interface này bằng việc sử dụng hàm Tools.compose (hàm compose sẽ được mô tả bên dưới) để lấy về interface đã được kết hợp r. Trong danh sách thành phần, đổi lại relational interface ở vị trí i thành r. Trong danh sách độ ưu tiên, xóa bỏ những độ ưu tiên có giá trị là max ra khỏi danh sách. Sau đó tiến hành bước 3. Bước 3: max ≔ max – 1, với max ≥ 0 quay trở lại bước 2. Ngược lại chuyển sang bước 4. Bước 4: Trả về interface mới được tạo ra từ việc kết hợp trên. Hàm public static RInterface compose (RInterface ri, ArrayList iarr): Tham chiếu của hàm ArrayList iarr cho ta biết, danh sách interface iarr là những interface song song, được kết nối vào interface ri. Vị trí kết nối của mỗi interface iarr[i] trong iarr với interface ri chính là thứ tự của i của iarr. Điều này có nghĩa là interface iarr[i] được kết nối vào input thứ i của ri. Nếu iarr[i] là null thì không có kết nối nào ở cổng input tương ứng. Đầu tiên, ta sẽ tiến hành kết nối song song tất cả các interface có trong iarr, tạo ra interface mới là para. Interface mới này có input là hợp của tất cả các input có trong iarr, output là hợp của tất cả các output có trong iarr, quan hệ ξ là hợp của tất cả quan hệ có trong iarr. Sau đó, hàm sẽ thực hiện việc kết hợp interface para với interface ri. Phép kết hợp được thực hiện ở đây là phép kết hợp bằng kết nối. Hàm này còn sử dụng 2 hàm là getInputAssumptionFormula và getPHIformula để phục vụ cho việc tính toán. Cách thức kết hợp đã được nêu ra trong phần 4.3.3. Hàm public static JavaMethod getMainMethod(JavaClass jc): nhiệm vụ của hàm này là lấy ra được phương thức main trong JavaClass. Cách thức hoạt động của hàm này đơn giản chỉ là so sánh tên từng JavaMethod trong JavaClass với “main”, nếu có trường hợp thỏa mãn thì trả về JavaMethod đó, ngược lại trả về null. Hàm public static RInterface getRInterfaceByName (String name, ArrayList ris): với tham chiếu truyền vào là name và ris, hàm sẽ tiến hành tìm trong danh sách RInterface ris, nếu có hàm sẽ trả về RInterface có tên là name, nếu không hàm trả về null. Hàm public static ArrayList getRInterfaceList(JavaClass jc): Hàm này được dùng để lấy ra danh sách những Rinterface từ JavaClass. Nội dung hàm này đơn giản như sau: public static ArrayList getRInterfaceList(JavaClass jc) { numOfRelation = 0; numOfInput = 0; ArrayListris = new ArrayList(); ArrayList jms = jc.methods; for (int i = 0; i < jms.size(); i++) { RInterface ri = new RInterface(jms.get(i), i); ris.add(ri); } return ris; } Hình 4.4: Hàm Tools. getRInterfaceList(JavaClass jc) Hàm public static String getInputAssumptionFormula(RInterface ri): Được sử dụng để tính input assumption của quan hệ ξ có trong ri. Cách thức tính đã được nêu ra trong phần 4.3.2. Hàm public static String getPHIformula(String relations, String in, Hashtable h): Được sử dụng để tính Φ của interface sau khi kết hợp. Cách thức tính đã được nêu ra trong phần 4.3. Lớp Expresstion.java Lớp Expression.java dùng để mô tả một biểu thức trong java với cấu trúc . Trong đó { =, !=, >, lưu trữ toán tử và toán hạng. Các hàm chính: Hàm public boolean hasOperand (String x): kiểm tra xem trong biểu thức có chưa toán hạng x hay không, nếu có thì trả về là true, ngược lại thì trả về false. Hàm public boolean hasOneOfOperands(ArrayList arr): Với tham chiếu truyền vào là danh sách tên các toán hạng. Hàm này sẽ kiểm tra xem biểu thức hiện thời có chứa một trong các toán hạng thuộc danh sách đó hay không. Nếu có thì trả về true, ngược lại trả về false. Hàm public static boolean isBooleanOperator(String x): dùng để kiểm tra xem String x có phải là một toán tử so sánh hay không, nếu có thì trả về true, ngược lại sẽ trả về false. Như đã nói ở trên, các toán tử so sánh bao gồm: { =, !=, >, <, ≥, ≤ }; Hàm public static Expression Combine(Expression e1, Expression e2, String operand): Hàm này được có tác dụng rút gọn toán hạng operand từ 2 biểu thức e1 và e2 và trả về biểu thức đã được rút gọn. Ví dụ với e1 ≔ a = b + 1, và e2 ≔ a = c, operand ≔ a. Biểu thức trả về sẽ là c = b + 1; Hàm public static ArrayList Shorten(ArrayList exps, Stack operands): Tương tự như hàm Combine, nhưng hàm này được sử dụng để rút gọn một số toán hạng từ những biểu thức cho trước, và trả về danh sách các biểu thức mới được tạo ra. Cách thức hoạt động của hàm này là lấy từng toán hạng trong stack ra, giả sử toán hạng op được lấy ra. Sau đó kiểm tra xem trong danh sách những biểu thức truyền vào, biểu thức nào có chứa toán hạng op thì sẽ đẩy những biểu thức này vào một ArrayList mới, tạm thời. Rồi sau đó sử dụng hàm Combine(Expression e1, Expression e2, String operand) để rút gọn từng cặp biểu thức một đến khi không còn toán hạng op. Ví dụ: Tập các biểu thức là: y1 = x1, y2 = x2 + 1, y1 = z1, y2 = z2, z1 = z2. Với tập toán hạng để rút gọn là { y1, y2, z1, z2 }. Giá trị trả về là x1 = x2 + 1. Nếu như trong quá trình rút gọn mà có một lúc nào đó vế trái bằng về phải thì giá trị trả về sẽ là null. Ví dụ: Tập các biểu thức là: y1 = x1, y2 = x1, y1 = z1, y2 = z2, z1 = z2. Với tập toán hạng để rút gọn là { y1, y2, z1, z2 }. Lúc này giá trị trả về là x1 = x1, tức là hệ các biểu thức luôn đúng. Không có ràng buộc nào được trả về, hàm return null; while (!operands.empty()) { ArrayList tmp = new ArrayList(); String opd = (String) operands.pop(); for (int i = exps.size() - 1; i >= 0; i--) { //System.out.println("1." + exps.get(i).toString()); if(exps.get(i).hasOperand(opd)&& exps.get(i).booleanOperator.equals(Expression.EQUAL)) { tmp.add(exps.get(i)); exps.remove(i); } } if (tmp.size() > 1) { for (int i = 1; i < tmp.size(); i++) { Expression e1 = Expression.Combine(tmp.get(0), tmp.get(i), opd); if (e1.left.equals(e1.right)) { return null; } exps.add(e1); } } } return exps; Hình 4.5: Hàm Shorten trong lớp Expression.java Lớp FOLOptimizer.java Lớp này được tạo ra nhằm mục đích tối ưu biểu thức logic. Phục vụ cho việc tính toán Φ, input assumption in(ϕ) một cách dễ dàng hơn. Hàm public static ArrayList Optimize(String str): với dữ liệu đầu vào là một biểu thức logic có kiểu là String, hàm này sẽ thực hiện việc chuyển biểu thức này thành một biểu thức tương đương ở dạng chuẩn tắc tuyển. Biểu thức mới tạo ra được tách thành các từ tố và là giá trị trả về của hàm. Ví dụ với String str = “( a | b ) & ( c | d )”, với “&” là phép AND, và “|” là phép OR. Hàm này sẽ chuyển str về dạng chuẩn tắc tuyển, String str1 mới ở dạng chuẩn tắc tuyển trong trường hợp này sẽ là: str1 = “a & c | a & d | b & c | b & d” CHƯƠNG 5: CÀI ĐẶT VÀ THỬ NGHIỆM Để minh họa cho công cụ chuyển đổi và kết hợp tự động các relational interface từ chương trước, chương này tôi sẽ mô tả chi tiết các bước cài đặt mà tôi đã thực hiện và kết quả thử nghiệm trên một số dữ liệu thực tế. Xây dựng công cụ Áp dụng phương pháp giải quyết bài toán đã được nêu ra ở chương trước, tôi đã xây dựng thành công công cụ chuyển đổi và kết hợp tự động relational interface từ java. Để xây dựng công cụ này, tôi đã sử dụng IDE* Netbeans (tại ) và framework JDK (Java Development Kit). Giao diện làm việc của Netbeans như sau: Hình 5.1: Giao diện làm việc của Netbeans Sau khi tiến hành xây dựng và biên dịch chương trình, tôi cài đặt công cụ của tôi dưới dạng một thư viện có tên là RelationalInterface.jar. Việc sử dụng thư viện này trên mỗi IDE khác nhau khá là giống nhau. Sau đây tôi sẽ minh họa việc cài đặt thư viện đối với IDE Netbeans. Hình 5.2: Minh họa cách cài đặt thư viện (1) Hình 5.3: Minh họa cách cài đặt thư viện (2) Sau khi tiến hành cài đặt thư viện vào một project (dự án) mới, ta có thể sử dụng các hàm, lớp mà công cụ này đã cung cấp để giải quyết bài toán. *IDE: International Development Enterprises – Môi trường phát triển tích hợp. Dữ liệu thử nghiệm Dữ liệu đưa vào là một file java có cấu trúc đơn giản, với các hàm cộng, trừ, nhân, chia, trị tuyệt đối và hàm main (Xem phụ lục 1). Nhiệm vụ của công cụ là phải đưa ra được relational interface cho mỗi phương thức cong, tru, nhan, chia, triTuyetDoi. Sau đó tiến hành việc kết hợp các interface này dựa theo thứ tự kết hợp các phương thức ở trong hàm main. Kết quả thử nghiệm Phân tích file mã nguồn Từ dữ liệu thử nghiệm trên, ta sử dụng công cụ để phân tích, tách file nguồn này những phương thức, thuộc tính của lớp. Kết quả thực nghiệm của quá trình này như sau: Hình 5.4: Kết quả thử nghiệm 5.3.1 đối với hàm main Hình 5.5: Kết quả thử nghiệm 5.3.1 đối với hàm cong Hình 5.6: Kết quả thử nghiệm 5.3.1 đối với hàm tru Hình 5.7: Kết quả thử nghiệm 5.3.1 đối với hàm nhan Hình 5.8: Kết quả thử nghiệm 5.3.1 đối với hàm chia Hình 5.9: Kết quả thử nghiệm 5.3.1 đối với hàm triTuyetDoi Trong đó: Method: là tên phương thức, Visibility: là mức độ truy cập, Type là kiểu của phương thức, Parameter là các tham chiếu truyền vào. Content: nội dung của phương thức. Như vậy, công cụ đã thực hiện việc phân tích nội dung file nguồn đúng, tốt. Chuyển những phương thức này thành relational interface Với mỗi phương thức như trên, ta sử dụng công cụ để tiến hành chuyển đổi chúng sang relational interface, xem xét kết quả chuyển đổi như sau: Đối với hàm cong, ta có interface Icong = ({x1, x2}, {y1}, y1 = x1 + x2) Hình 5.10: Kết quả thử nghiệm 5.3.2 với hàm cong Đối với hàm tru, ta có interface Itru = ({x3, x4}, {y2}, y2 = x3 – x4) Hình 5.11: Kết quả thử nghiệm 5.3.2 đối với hàm tru Đối với hàm nhan, ta có interface Inhan = ({x5, x6}, {y3}, y3 = x5 * x6) Hình 5.12: Kết quả thử nghiệm 5.3.2 đối với hàm nhan Đối với hàm chia, ta có interface Ichia = ({x7, x8}, {y4}, x8 != 0 ∧ y4 = x7 / x8) Hình 5.13: Kết quả thử nghiệm 5.3.2 đối với hàm chia Đối với hàm triTuyetDoi, ta có interface Ittd = ({x9}, {y5}, x9 ≥ 0 ∧ y5 = x9 ∨ (!x9 ≤ 0) ∧ y5 = - x9) Hình 5.14: Kết quả thử nghiệm 5.3.2 đối với hàm triTuyetDoi Trong đó: Name: tên interface, Inputs: là tập input, Ouput: là tập output, Relation là quan hệ giữa input và output. Như vậy, công cụ đã tiến hành chuyển đổi đúng mỗi phương thức ở trên thành các interface tương ứng. Kết hợp các interface Bước cuối cùng, ta sẽ sử dụng công cụ để tiến hành việc kết hợp các interface Icong, Itru, Inhan, Ichia, Ittd lại với nhau theo thứ tự kết hợp được đưa ra ở hàm main. Ở đây, ta có 2 phép kết hợp là: chia(cong(a, b), tru(a, b)) và triTuyetDoi(tru(a, b)) result1 = chia(cong(a, b), tru(a, b)); Với: Icong = ({x1, x2}, {y1}, y1 = x1 + x2) Itru = ({x3, x4}, {y2}, y2 = x3 – x4) Inhan = ({x5, x6}, {y3}, y3 = x5 * x6) Ichia = ({x7, x8}, {y4}, x8 != 0 ∧ y4 = x7 / x8) Ittd = ({x9}, {y5}, x9 ≥ 0 ∧ y5 = x9 ∨ (!x9 ≤ 0) ∧ y5 = - x9) Đối với phép kết hợp chia(cong(a, b), tru(a, b)) Icong Itru Ichia x1 x2 y1 y2 x3 x4 x7 x8 y4 Hình 5.15: Biểu đồ interface cho kết hợp chia(cong(a, b), tru(a, b)) Từ biểu đồ ở hình 23 ta có phép kết hợp: (θ1 ∪ θ2)((Icong || Itru) , Ichia) Trong đó, θ1 ≔ {y1, x7} và θ2 ≔ {y2, x8}. Định nghĩa θ3 ≔ θ1 ∪ θ2. Bằng phép kết hợp song song giữa Icong và Itru ta có: Icong || Itru = ({x1, x2, x3, x4}, {y1, y2}, y1 = x1 + x2, y2 = x3 – x4) Mặt khác: in(Ichia) ≡ x8 != 0. Do đó, với θ3((Icong || Itru) , Ichia), ta có: Φ ≔ (y1 = x1 + x2 ∧ y2 = x3 – x4 ∧ y1 = x7, y2 = x8) → x8 != 0. Rút gọn đi, ta được: ∀ y1, y2, x7, x8 : Φ ≡ x3 – x4 != 0. Do vậy: θ3((Icong || Itru) , Ichia) = ({x1, x2, x3, x4}, {y1, y2, y4, x7, x8}, y1 = x1 + x2 ∧ y2 = x3 - x4 ∧ y1 = x7 ∧ y2 = x8 ∧ x8 != 0 ∧ y4 = x7 / x8 ∧ x3 – x4 != 0). Sau đây, ta sẽ xem xét kết quả mà quá trình kết hợp tự động của công cụ: Hình 5.16: Kết quả thử nghiệm 5.3.3 đối với hàm main Như vậy, interface sau khi được kết hợp tự động giống với interface mà ta đã tính toán ở trên. Dự đoán kết quả: Ta có: θ3((Icong || Itru) , Ichia) = ({x1, x2, x3, x4}, {y1, y2, y4, x7, x8}, y1 = x1 + x2 ∧ y2 = x3 - x4 ∧ y1 = x7 ∧ y2 = x8 ∧ x8 != 0 ∧ y4 = x7 / x8 ∧ x3 – x4 != 0) (*). Quay trở lại với đoạn mã trong hàm main: result1 = chia(cong(a, b), tru(a, b)); Ở đây, x1 = x3 = a, x2 = x4 = b. Với a = 4, b = 2, ta có: result1 = 3; Từ (*), với x1 = x3 = 4, x2 = x4 = 2, ta có: y1 = 6, y2 = 2, x7 = 6, x8 = 2, x8 = 2 != 0, y4 = 3, x3 – x4 = 2 != 0. Do vậy phép kết hợp này là hoàn toàn thỏa mãn. Với a = 2, b = 2, khi biên dịch, chương trình sẽ “ném” ra một ngoại lệ. Tức là phép tính không thỏa mãn. Từ (*), với x1 = x3 = 2, x2 = x4 = 2, ta có: y1 = 4, y2 = 0, x7 = 4, x8 = 0, y4 = 3, x8 = 0 != 0, x3 – x4 = 0 != 0. Trong trường hợp này, do 0 != 0 ≔ false, phép kết hợp này là không thỏa mãn. Như vậy, thông qua interface sau khi kết hợp, ta có thể dự đoán chính xác được kết quả trả về của việc kết hợp các thành phần, vì interface mới tạo ra vẫn giữ nguyên được các tính chất của interface thành phần. Đánh giá Qua kết quả thử nghiệm của công cụ cho thấy, chương trình đã hoạt động tốt trên từng mô-đun, đưa ra kết quả cuối cùng của bài toán là đúng. Đáp ứng được yêu cầu, mục tiêu mà bài toán đã đặt ra trước đó. CHƯƠNG 6: KẾT LUẬN Kết luận về khóa luận Trong quá trình thực hiện khóa luận này, bằng việc tìm hiểu những kiến thức cơ bản về kỹ nghệ hướng thành phần, thiết kế dựa trên thành phần, và kiến thức về interface. Tôi đưa ra được phương pháp thiết kế phần mềm dựa trên các interface. Đồng thời, tôi cũng đã xây dựng một công cụ tự động phân tích, chuyển đổi từ những phương thức có trong file mã nguồn của một ngôn ngữ lập trình hướng đối tượng thành những relational interface tương ứng. Công cụ này cũng có chức năng kết hợp tự động các interface này lại với nhau và đưa ra được interface tổng hợp. Với công cụ này, ta có thể tiến hành xem xét các khả năng kết hợp giữa các thành phần, cụ thể là các phương thức trong file mã nguồn java. Thông qua interface, ta còn biết được các tính chất của mỗi thành phần. Từ đó, giúp ta dự đoán một cách chính xác kết quả đầu ra thông qua các tính chất này. Tuy nhiên, công cụ này vẫn còn một số những hạn chế như: Chỉ phân tích được file mã nguồn có cấu trúc đơn giản. Chưa hỗ trợ việc kết hợp bằng phản hồi (Composition by Feedback). Chưa có giao diện đồ họa. Chưa tự động kiểm tra được tính chất thỏa mãn của công thức ξ. Hướng phát triển trong tương lai Từ những vấn đề còn tồn đọng trong khóa luận này, trong tương lai tôi sẽ tiếp tục nghiên cứu này nhằm xây dựng hoàn thiện công cụ để đáp ứng tốt hơn nữa những yêu cầu đặt ra. Cụ thể: Tôi sẽ phát triển tiếp để công cụ có thể bắt được những ràng buộc, quan hệ đặc trưng của thành phần có trong file mã nguồn với cấu trúc phức tạp. Ngoài ra việc dữ liệu đầu vào có thể được mở rộng với mã nguồn của một vài ngôn ngữ lập trình khác. Hỗ trợ việc kết hợp bằng phản hồi (Composition by Feedback) Tự động kiểm tra tính chất thỏa mãn của công thức ξ bằng việc sử dụng các solver có sẵn như: SAT solver, Z3. Xây dựng giao diện đồ họa . Tôi hi vọng, ứng dụng của tôi sẽ góp phần cho việc phát triển ngành công nghệ phần mềm nói riêng và ngành công nghệ thông tin nói chung hiện nay. Phụ lục Phụ lục 1: Nội dung mã nguồn file thử nghiệm Sample.java public class Sample { public static void main(String[] args) throws Exception { float a = 2; float b = 3; float result1; result1 = chia(cong(a, b), tru(a, b)); } public static float cong(float a, float b) { return a + b; } public static float tru(float a, float b) { return a - b; } public static float nhan(float a, float b) { return a * b; } public static float chia(float a, float b) throws Exception { if (b != 0) { return a / b; } else { throw new Exception(); } } public static float triTuyetDoi(float a) { if (a >= 0) { return a; } else { return -a; } } } TÀI LIỆU THAM KHẢO [1] Đỗ Đức Giáo. Hướng dẫn giải bài tập toán rời rạc. NXB Giáo dục, Hà Nội, 2007, tr.276-277. [2] A. Chakrabarti, L. de Alfaro, T. Henzinger, and F. Mang. Synchronous and bidirectional component interfaces. In CAV, LNCS 2404, Springer, 2002. Tr.414-427. [3] Ian Sommerville. Software Engineering 6th Edition. 2001. Tr.193-197. [4] L. de Alfaro and T.Henzinger. Interface Automata. In Foundations of Software Engineering (FSE). ACM Press, 2001. [5] Luca de Alfaro, Thomas A. Henzinger. Interface Theories for Component-based design. In Proceedings of the First International Workshop on Embedded Software (EMSOFT), 2001. [6] L. Doyen, T.Henzinger, B.Jobstmanm, and T.Petrov. Interface theories with component reuse. In 8th ACM IEEE International conference on Embedded software, EMSOFT. Tr.79-88, 2008. [7] Stavros Tripakis, Ben Lickly, Thomas A.Henzinger, Edward A.Lee. On relational interfaces. In EMSOFT’09, October 12-16, 2009, Grenoble, France. [8] Wikimedia.com. [9] Wikimedia.com.