Khóa luận Ứng dụng Relational Interface cho Java

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