Một số tính toán và làm mịn với các thành phần

Nguyễn Mạnh Đức<br /> <br /> Tạp chí KHOA HỌC & CÔNG NGHỆ<br /> <br /> 78(02): 97 - 104<br /> <br /> MỘT SỐ TÍNH TOÁN VÀ LÀM MỊN VỚI CÁC THÀNH PHẦN<br /> Nguyễn Mạnh Đức<br /> Khoa Toán, Trường Đại học Sư phạm – Đại học Thái Nguyên<br /> <br /> TÓM TẮT<br /> Trong bài báo chúng tôi sẽ trình bày một cách hình thức một số khái niệm cơ bản quan trọng cho<br /> mô hình phát triển phần mềm thành phần, bao gồm giao diện, các hợp đồng, các giao thức tƣơng<br /> tác, các thành phần và những quan hệ giữa các khái niệm đó, các tính toán làm mịn giữa chúng với<br /> nhau. Các đặc tả và các tính toán làm mịn đƣợc thực hiện dựa theo mô hình tính toán rCOS, để bảo<br /> đảm tính đúng đắn và nhất quán của hệ thống. Những công việc này có thể đƣợc thực hiện trong<br /> các giai đoạn khác nhau của tiến trình phát triển phần mềm. Từ đó cho thấy ý nghĩa và sự cần thiết<br /> khi phát triển phƣơng pháp hình thức trong kỹ nghệ phần mềm hƣớng thành phần.<br /> Từ khóa: Làm mịn hệ thống đối tượng và thành phần , thiết kế , giao diện, hợp đồng, thành phần,<br /> ngôn ngữ mô hình hóa thống nhất UML<br /> <br /> GIỚI THIỆU*<br /> Sử dụng các thành phần để xây dựng và bảo<br /> trì các hệ thống phần mềm không phải là ý<br /> tƣởng mới. Tuy nhiên, do độ phức tạp của các<br /> hệ thống trong ngày nay đang tăng lên nhanh,<br /> điều đó đã buộc chúng ta phải trở lại với ý<br /> tƣởng này trong thực tế [3]. Các kỹ thuật dựa<br /> trên công nghệ hƣớng đối tƣợng và thành<br /> phần đã trở nên phổ biến và đƣợc sử dụng<br /> rộng rãi để mô hình hóa và thiết kế các hệ<br /> thống phần mềm lớn và phức tạp. Chúng cung<br /> cấp sự hỗ trợ hiệu quả để phân tách một ứng<br /> dụng thành các đối tƣợng và thành phần, phục<br /> vụ hữu hiệu cho việc sử dụng lại, mở rộng<br /> những thiết kế đã có và cài đặt mới… Các<br /> công việc phân tích và kiểm tra hệ thống phức<br /> hợp có thể sẽ dễ dàng hơn do kiến trúc của hệ<br /> thống thành phần [5].<br /> Thiết kế và phát triển hệ thống phần mềm với<br /> ngôn ngữ hƣớng đối tƣợng đã đƣợc thừa nhận<br /> là rất phức tạp [2]. Phát triển phần mềm theo<br /> hƣớng thành phần là bƣớc phát triển logic tiếp<br /> theo của phƣơng pháp hƣớng đối tƣợng.<br /> Nhiều nhà nghiên cứu đã chỉ ra sự cần thiết<br /> phát triển công cụ hình thức hoá làm nền tảng<br /> cho việc phát triển phần mềm hƣớng đối<br /> tƣợng và hƣớng thành phần. Trong bài báo<br /> này chúng ta xem xét kỹ thuật mô hình hóa<br /> mà nó hỗ trợ sự đặc tả các hệ thống đối tƣợng<br /> và thành phần ở mức trừu tƣợng cao, dựa trên<br /> *<br /> <br /> Tel: 0915 564 249; Email: nmductn@yahoo.com<br /> <br /> lý thuyết lập trình thống nhất của Hoare và<br /> He [1, 5]. Đề xuất một số vấn đề phục vụ cho<br /> việc thiết kế và phát triển các hệ thống thành<br /> phần, dùng cho việc xây dựng một cách đúng<br /> đắn các chƣơng trình hƣớng thành phần.<br /> Sau phần giới thiệu, phần 2 trình bày khái<br /> niệm giao diện (interface), phần 3 trình bày<br /> khái niệm hợp đồng (contract), phần 4 trình<br /> bày khái niệm về thành phần (component).<br /> Trong mỗi phần chúng tôi sẽ đƣa ra các thảo<br /> luận, một số tính chất và các ngữ nghĩa, mối<br /> quan hệ giữa chúng và các tính toán làm mịn<br /> liên quan. Trong phần 5 sẽ đƣa ra một số<br /> nhận xét và kết luận về các công việc mà mà<br /> chúng tôi đã tiến hành.<br /> GIAO DIỆN (INTERFACES)<br /> Giao diện của một thành phần có thể đƣợc<br /> định nghĩa nhƣ là sự đặc tả điểm truy nhập<br /> của thành phần đó [4]. Các khách hàng truy<br /> nhập tới các dịch vụ đƣợc cung cấp bởi một<br /> thành phần bằng cách sử dụng các điểm truy<br /> nhập này. Nếu một thành phần có nhiều điểm<br /> truy nhập, mỗi điểm truy nhập đó biểu diễn<br /> cho các dịch vụ khác đƣợc đƣa ra bởi thành<br /> phần, thì thành phần đƣợc mở rộng phải có<br /> nhiều giao diện.<br /> Interface là một tập hợp các đặc trƣng, ở đây<br /> đặc trƣng có thể là trƣờng hoặc phƣơng thức.<br /> Một cách hình thức, ta có thể định nghĩa<br /> Interface nhƣ sau.<br /> Định nghĩa (Interface): Interface là cặp khai<br /> báo đặc các trưng I = . Trong<br /> 97<br /> <br /> Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên<br /> <br /> http://www.lrc-tnu.edu.vn<br /> <br /> Nguyễn Mạnh Đức<br /> <br /> Tạp chí KHOA HỌC & CÔNG NGHỆ<br /> <br /> đó FDec là tập các khai báo trường, được ký<br /> hiệu là I.FDec; MDec là tập các khai báo<br /> phương thức, được ký hiệu là I.MDec.<br /> Mỗi thành viên của FDec có dạng x: T, ở đây<br /> x là tên và T là kiểu của trƣờng đƣợc khai<br /> báo. Không đƣợc khai báo các trƣờng trùng<br /> tên trong cùng một FDec.<br /> Một phƣơng thức (phép toán) trong MDec có<br /> dạng m(in inx, out outx), trong đó m là tên của<br /> phƣơng thức, inx là danh sách các tham số<br /> vào, outx là danh sách các tham số ra; Mỗi<br /> một khai báo tham số vào hoặc ra có dạng u:<br /> U là tên và kiểu của tham số.<br /> Tên của phƣơng thức cùng với các tham số<br /> cùng với các kiểu của các tham số vào và ra<br /> tạo thành ký danh của phƣơng thức. Nói<br /> chung cả inx và outx có thể trống. Để đơn<br /> giản hóa và không làm mất tính tổng quát,<br /> chúng ta có thể biểu diễn lại phƣơng thức ở<br /> dạng m(in: U, out: V) bằng cách bỏ đi các từ<br /> khóa inx và outx, do đó có thể coi m(in1: U,<br /> out1: V) và m(in2: U, out2: V) là các phƣơng<br /> thức cùng một ký danh. Đơn giản hơn có thể<br /> biểu diễn một phƣơng thức của Interface là<br /> m(u, v), với u và v là các tham số vào và ra<br /> của m.<br /> Trong một Interface không thực thi bất kỳ<br /> một phƣơng thức nào của nó, thay vì đó chỉ là<br /> các tên của các phƣơng thức cùng với các<br /> tham số để cung cấp các ký danh cho những<br /> phép toán của chúng.<br /> Ví dụ 1: Một bộ đệm của các số nguyên, giao<br /> diện của nó có khả năng cho ngƣời sử dụng<br /> đặt vào và lấy ra dữ liệu từ nó. Ta có thể biểu<br /> diễn giao diện này nhƣ sau:<br /> IBuff = <br /> ở đây seq(int) là kiểu dãy hữu hạn có thứ tự<br /> của các số nguyên và chúng ta qui ƣớc có thể<br /> dùng các ký pháp chuẩn để chỉ độ dài, phần<br /> tử đầu tiên hay cuối cùng… của dãy.<br /> Định nghĩa (tính gộp lại): Hai Interface là<br /> có khả năng gộp lại (composable) nếu chúng<br /> không sử dụng cùng một tên trường với các<br /> kiểu khác nhau.<br /> Giả sử I và J là các Interface có khả năng<br /> gộp lại, kí pháp I ⊕ J biểu diễn một interface<br /> <br /> 78(02): 97 - 104<br /> <br /> với các thành phần trường và phương thức<br /> như sau:<br /> (I ⊕ J).FDec def I. FDec ∪<br /> J.FDec<br /> (I ⊕ J).MDec def I.MDec1 ∪<br /> J.MDec<br /> Theo định nghĩa trên ta có các tính chất sau<br /> với các Interface có tính gộp lại:<br /> (1) I ⊕ I = I<br /> (2) I⊕ J = J⊕ I<br /> (3) I1⊕ (I2⊕ I3 ) = (I1⊕ I2)⊕ I3<br /> Ta có thể dễ dàng chứng minh các tính chất<br /> này nhƣ sau:<br /> (1) Theo tính chất lũy đẳng của<br /> các phép toán tập hợp.<br /> (2) Theo tính chất giao hoán của<br /> các phép toán tập hợp.<br /> (3) Theo tính chất kết hợp của<br /> các phép toán tập hợp.<br /> Sự kế thừa interface: Kế thừa (inheritance)<br /> là các phƣơng tiện có ích cho sử dụng lại và<br /> lập trình gia tăng. Khi thành phần cung cấp<br /> chỉ một nhiệm vụ của các dịch vụ cần thiết<br /> hoặc một số phép toán đƣợc cung cấp là<br /> không đủ phù hợp cho sự cần thiết, chúng ta<br /> có thể sử dụng thành phần này bằng cách viết<br /> lại một số phép toán hoặc mở rộng nó với một<br /> số phép toán xử lý và các thuộc tính.<br /> Định nghĩa (kế thừa Interface): Cho I và J<br /> là các Interface, giả thiết rằng không có<br /> trường nào của J được định nghĩa lại trong I.<br /> Ký pháp I extends J biểu diễn một Interface<br /> có các miền trường và phương thức như sau:<br /> (I extends J).FDec def I.FDec ∪<br /> J.FDec<br /> (I extends J).MDec def I.MDec ∪<br /> {m(in: U, out: V)|m ∈ J.MDec∧ op ∉<br /> I.MDec}<br /> Theo định nghĩa này, ta có các tính chất sau:<br /> (1) I extends (J1⊕ J2 ) = (I<br /> extends J1)⊕ (I extends J2)<br /> (2) (I1⊕ I2 ) extends J = (I1<br /> extends J)⊕ (I2 extends J)<br /> Ta có thể chứng minh các tính chất này<br /> nhƣ sau:<br /> <br /> 98<br /> <br /> Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên<br /> <br /> http://www.lrc-tnu.edu.vn<br /> <br /> Nguyễn Mạnh Đức<br /> <br /> Tạp chí KHOA HỌC & CÔNG NGHỆ<br /> <br /> (1) Theo tính chất kết hợp của các phép toán<br /> tập hợp và do<br /> (U \ V1 ) ∪ (U \ V2) = U \ (V1 ∪ V2)<br /> (2) Theo tính chất kết hợp của các phép toán<br /> tập hợp và do<br /> (U1 \ V ) ∪ (U2 \ V) = (U1 ∪ U2) \ V<br /> Sự làm ẩn (hiding): Để có thể đƣa ra các<br /> dịch vụ khác nhau cho các khách hàng khác<br /> nhau của một thành phần, chúng ta cho phép<br /> làm ẩn các phép toán trong một interface để<br /> không nhìn thấy chúng khi một thành phần<br /> đƣợc bao bởi các thành phần nào đó. Việc<br /> làm ẩn các toán tử cung cấp hiệu ứng ngƣợc<br /> với kế thừa giao diện và đƣợc sử dụng để giới<br /> hạn giao diện. Trong ký pháp đồ họa nhƣ<br /> UML, vấn đề này có thể thực hiện đƣợc bằng<br /> ký pháp tổng quát hóa [3, 9].<br /> Định nghĩa (sự làm ẩn|sự che dấu): Giả sử I<br /> là interface và S là tập các tên phương thức.<br /> Ký pháp I\S chỉ interface I sau khi loại bỏ các<br /> phương thức của S từ phần khai báo phương<br /> thức của nó:<br /> (I\S).FDec def I.FDec<br /> (I\S).MDec def I.MDec \ S<br /> Việc làm ẩn các phép toán có các tính chất<br /> sau:<br /> (1) (I \ S1) \ S2 = I \ (S1 ∪ S2)<br /> (2) I \ ∅ = I<br /> (3) (I1 ⊕ I2) \ S = (I1 \ S) ⊕ (I2 \ S)<br /> (4) (I extends J) \ S = (I \ S) extends (J \ S)<br /> Chứng minh: giả sử U, U1, U2, V, V1, V2 là các<br /> tập hợp, ta có:<br /> (1) đƣợc thỏa mãn do (U \ V1 ) \ V2 = U \<br /> (V1 ∪ V2)<br /> (2) đƣợc thỏa mãn do U \ ∅ = U<br /> (3) đƣợc thỏa mãn do (U1 ∪ U2) \ V = (U1<br /> \ V) ∪ (U2 \ V)<br /> (4) đƣợc thỏa mãn do (U1 ∪ (U2 \ U1)) \ V<br /> = ((U1 \ V) ∪ (U2 \ V)) \ (U1 \ V).<br /> Từ (1) cho thấy rằng thứ tự của các phép<br /> toán trong 2 tập không quan trọng. Từ (3)<br /> ta thấy sự làm ẩn có tính phân phối với các<br /> toán hạng trong interface. Dựa vào các tính<br /> chất trên, một số các tính toán làm mịn của<br /> contract và thành phần đã đƣợc xây dựng<br /> và thực hiện [7, 8, 9].<br /> <br /> 78(02): 97 - 104<br /> <br /> HỢP ĐỒNG (CONTRACT)<br /> Hợp đồng (Contract) là ngữ nghĩa đặc tả các<br /> chức năng cho Interface. Đó là sự giao ƣớc<br /> quan hệ của một giao diện tới một ứng dụng<br /> bằng mô hình dữ liệu (trừu tƣợng) có tính rõ<br /> ràng, cụ thể, mô tả các chức năng của các<br /> toán tử dịch vụ, các giao thức đặc trƣng, và<br /> bảo đảm các chất lƣợng yêu cầu khác của các<br /> dịch vụ tùy thuộc vào ứng dụng. Mô hình<br /> cũng cung cấp định nghĩa nhất quán giữa các<br /> khung nhìn và phƣơng thức kiểm tra tính nhất<br /> quán này. Sự liên quan có thể mở rộng theo<br /> chiều ngang bằng cách bổ sung nhiều hơn các<br /> dịch vụ, các tính chất để bảo đảm chất lƣợng<br /> dịch vụ [3].<br /> Sự đặc tả một phƣơng thức của một Interface<br /> là thiết kế D = (, P) [1], ở đây :<br />  là tập của các biến (cùng với kiểu của<br /> chúng) đƣợc sử dụng bởi phƣơng thức chứa<br /> trong các tham biến vào và ra.<br /> P là tân từ có dạng (p ⊢ R) def (ok ∧<br /> p)  (ok’ ∧ R) đƣợc sử dụng để mô tả các<br /> hành vi của phƣơng thức. p là tiền điều kiện,<br /> trạng thái khởi tạo đƣợc chấp nhận là đúng để<br /> nhờ đó mà phƣơng thức đƣợc kích hoạt và<br /> đƣợc biểu diễn bởi tập {x | x ∈ ( \ {out})}<br /> của các biến. Tân từ R đƣợc gọi là hậu điều<br /> kiện, xác định quan hệ các trạng thái khởi đầu<br /> tới các trạng thái cuối cùng và đƣợc mô tả bởi<br /> tập {x’ | x ∈ ( \ {in})}.<br /> Thiết kế D1 đƣợc làm mịn bởi thiết kế D2 (ký<br /> hiệu là D1 ⊑ D2) nếu:<br /> ok, ok’, v, v’ •<br /> (D2 D1)<br /> Một cách hình thức, contract đƣợc định nghĩa<br /> nhƣ dƣới đây.<br /> Định nghĩa (contract): Contract là cặp Ctr<br /> = (I, Init, MSpec, Prot), trong đó:<br /> 1. I là một Interface.<br /> 2. Init là hàm xác định các giá trị khởi đầu<br /> cho các trường đã khai báo trong I.FDec.<br /> 3. MSpec là ánh xạ mỗi phương thức m(in:<br /> U, out: V) của I tới sự đặc tả của nó là thiết<br /> kế với tập alphabet α, ở đây:<br /> inα def {in} ∪ I.FDec, outα def {out’} ∪<br /> I.FDec’, α = inα ∪ outα.<br /> 99<br /> <br /> Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên<br /> <br /> http://www.lrc-tnu.edu.vn<br /> <br /> Nguyễn Mạnh Đức<br /> <br /> Tạp chí KHOA HỌC & CÔNG NGHỆ<br /> <br /> 4. Prot được gọi là giao thức của Interface,<br /> đó là tập các dãy hữu hạn có thứ tự của các<br /> sự kiện gọi phương thức. Dãy hữu hạn này có<br /> dạng m1, m2, …, mk.<br /> Ý nghĩa của contract là:<br /> 1. Nếu ngƣời sử dụng các thành phần tuân<br /> theo giao thức khi tƣơng tác với thành phần,<br /> thì sẽ không xuất hiện các trạng thái đình trệ<br /> cũng nhƣ sai lệch, và<br /> 2. Tại mọi thời điểm khi ngƣời sử dụng gọi<br /> phép toán trong giao thức, trạng thái thay đổi<br /> và trả lại giá trị sẽ phù hợp trạng thái đặc tả<br /> chức năng của phép toán.<br /> Với nhiều ứng dụng, các giao thức có thể<br /> đƣợc chỉ rõ bởi các biểu thức chuẩn mực và<br /> trong trƣờng hợp thuận tiện có thể đƣợc kiểm<br /> tra tự động [3].<br /> Ví dụ 2: Với giao diện của bộ đệm các số<br /> nguyên trong ví dụ 1, Một contract CtrBuff<br /> với giao diện của bộ đệm này có thể xác định<br /> nhƣ sau:<br /> CtrBuff.IBuff = IBuff<br /> như trong ví dụ 1<br /> <br /> // xác định<br /> <br /> CtrBuff.Init = |buff| = 0<br /> CtrBuff.MSpec(put(in x: int)) def (true ⊢<br /> buff’ = )<br /> CtrBuff.MSpec(get(out y: int)) def (true ⊢<br /> buff =  out’ = head(buff))<br /> CtrBuff.Prot = (put; get)* + (put; (get;<br /> put)*)<br /> Định nghĩa (reactive contract): Một<br /> contract tác động trở lại (reactive contract)<br /> là bộ ba Ctr = (I, Init, MSpec), ở đây MSpec<br /> gắn mỗi phép toán m(x, y) trong interface I<br /> với một thiết kế bị chặn.<br /> Ví dụ 3: Con tract trong ví dụ 2 có thể coi nhƣ<br /> contract tác động lại nhƣ sau:<br /> CtrBuff.I = IBuff<br /> // xác định<br /> như trong ví dụ 2<br /> CtrBuff.Init = |buff| = 0<br /> CtrBuff.MSpec(put(in x: int))<br /> = 0) & (true ⊢ buff’ = )<br /> <br /> def (|buff|<br /> <br /> CtrBuff.MSpec(get(out y: int)) def (|buff|<br /> > 0) & (true ⊢ buff’ =  y’ = head(buff))<br /> <br /> 78(02): 97 - 104<br /> <br /> Cho contract tác động lại Ctr = (I, Init,<br /> MSpec), hành vi động của nó đƣợc xác định<br /> bởi các tập các trạng thái không phù hợp và<br /> sai lệch F(Ctr) và D(Ctr). Mỗi phƣơng thức<br /> gọi m(u, v) bao gồm hai sự kiện ?m(u) để tiếp<br /> nhận yêu cầu và m(v)! để gửi trả lại cho lời<br /> gọi, cho nên mỗi vết của các trạng thái không<br /> phù hợp và sai lệch có dạng:<br /> ?m1(u1), m1(v1)!, …, ?mn(un),<br /> mn(vn)! và ?m1(u1), m1(v1)!, …,<br /> ?mn(un)<br /> Các trạng thái không phù hợp và sai lệch<br /> đƣợc xác định nhƣ sau [6]:<br />  D(Ctr) bao gồm các dãy có thứ tự của các<br /> tƣơng tác giữa Ctr và môi trƣờng của nó dẫn<br /> contract tới trạng thái sai lệch.<br />  F(Ctr) là tập của các cặp (s, X), ở đây s là<br /> dãy thứ tự của các tƣơng tác giữa Ctr và môi<br /> trƣờng của nó, X là tập các phƣơng thức để<br /> contract có thể từ chối trả lời sau khi thực<br /> hiện s. Một trạng thái không phù hợp (s, X) sẽ<br /> là một trong các trƣờng hợp sau đây:<br /> 1. s =