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 Tạp chí KHOA HỌC & CÔNG NGHỆ 78(02): 97 - 104 97 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 Khoa Toán, Trường Đại học Sư phạm – Đại học Thái Nguyên TÓM TẮT 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 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 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 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 đả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 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 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. 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, ngôn ngữ mô hình hóa thống nhất UML GIỚI THIỆU* Sử dụng các thành phần để xây dựng và bảo trì các hệ thống phần mềm không phải là ý tƣởng mới. Tuy nhiên, do độ phức tạp của các hệ thống trong ngày nay đang tăng lên nhanh, điều đó đã buộc chúng ta phải trở lại với ý tƣởng này trong thực tế [3]. Các kỹ thuật dựa trên công nghệ hƣớng đối tƣợng và thành phần đã trở nên phổ biến và đƣợc sử dụng rộng rãi để mô hình hóa và thiết kế các hệ thống phần mềm lớn và phức tạp. Chúng cung cấp sự hỗ trợ hiệu quả để phân tách một ứng dụng thành các đối tƣợng và thành phần, phục vụ hữu hiệu cho việc sử dụng lại, mở rộng những thiết kế đã có và cài đặt mới Các công việc phân tích và kiểm tra hệ thống phức hợp có thể sẽ dễ dàng hơn do kiến trúc của hệ thống thành phần [5]. Thiết kế và phát triển hệ thống phần mềm với ngôn ngữ hƣớng đối tƣợng đã đƣợc thừa nhận là rất phức tạp [2]. Phát triển phần mềm theo hƣớng thành phần là bƣớc phát triển logic tiếp theo của phƣơng pháp hƣớng đối tƣợng. Nhiều nhà nghiên cứu đã chỉ ra sự cần thiết phát triển công cụ hình thức hoá làm nền tảng cho việc phát triển phần mềm hƣớng đối tƣợng và hƣớng thành phần. Trong bài báo này chúng ta xem xét kỹ thuật mô hình hóa mà nó hỗ trợ sự đặc tả các hệ thống đối tƣợng và thành phần ở mức trừu tƣợng cao, dựa trên * Tel: 0915 564 249; Email: nmductn@yahoo.com lý thuyết lập trình thống nhất của Hoare và He [1, 5]. Đề xuất một số vấn đề phục vụ cho việc thiết kế và phát triển các hệ thống thành phần, dùng cho việc xây dựng một cách đúng đắn các chƣơng trình hƣớng thành phần. Sau phần giới thiệu, phần 2 trình bày khái niệm giao diện (interface), phần 3 trình bày khái niệm hợp đồng (contract), phần 4 trình bày khái niệm về thành phần (component). Trong mỗi phần chúng tôi sẽ đƣa ra các thảo luận, một số tính chất và các ngữ nghĩa, mối quan hệ giữa chúng và các tính toán làm mịn liên quan. Trong phần 5 sẽ đƣa ra một số nhận xét và kết luận về các công việc mà mà chúng tôi đã tiến hành. GIAO DIỆN (INTERFACES) Giao diện của một thành phần có thể đƣợc định nghĩa nhƣ là sự đặc tả điểm truy nhập của thành phần đó [4]. Các khách hàng truy nhập tới các dịch vụ đƣợc cung cấp bởi một thành phần bằng cách sử dụng các điểm truy nhập này. Nếu một thành phần có nhiều điểm truy nhập, mỗi điểm truy nhập đó biểu diễn cho các dịch vụ khác đƣợc đƣa ra bởi thành phần, thì thành phần đƣợc mở rộng phải có nhiều giao diện. Interface là một tập hợp các đặc trƣng, ở đây đặc trƣng có thể là trƣờng hoặc phƣơng thức. Một cách hình thức, ta có thể định nghĩa Interface nhƣ sau. Định nghĩa (Interface): Interface là cặp khai báo đặc các trưng I = . Trong Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên Nguyễn Mạnh Đức Tạp chí KHOA HỌC & CÔNG NGHỆ 78(02): 97 - 104 98 đó FDec là tập các khai báo trường, được ký hiệu là I.FDec; MDec là tập các khai báo phương thức, được ký hiệu là I.MDec. Mỗi thành viên của FDec có dạng x: T, ở đây x là tên và T là kiểu của trƣờng đƣợc khai báo. Không đƣợc khai báo các trƣờng trùng tên trong cùng một FDec. Một phƣơng thức (phép toán) trong MDec có dạng m(in inx, out outx), trong đó m là tên của phƣơng thức, inx là danh sách các tham số vào, outx là danh sách các tham số ra; Mỗi một khai báo tham số vào hoặc ra có dạng u: U là tên và kiểu của tham số. Tên của phƣơng thức cùng với các tham số cùng với các kiểu của các tham số vào và ra tạo thành ký danh của phƣơng thức. Nói chung cả inx và outx có thể trống. Để đơn giản hóa và không làm mất tính tổng quát, chúng ta có thể biểu diễn lại phƣơng thức ở dạng m(in: U, out: V) bằng cách bỏ đi các từ khóa inx và outx, do đó có thể coi m(in1: U, out1: V) và m(in2: U, out2: V) là các phƣơng thức cùng một ký danh. Đơn giản hơn có thể biểu diễn một phƣơng thức của Interface là m(u, v), với u và v là các tham số vào và ra của m. Trong một Interface không thực thi bất kỳ một phƣơng thức nào của nó, thay vì đó chỉ là các tên của các phƣơng thức cùng với các tham số để cung cấp các ký danh cho những phép toán của chúng. Ví dụ 1: Một bộ đệm của các số nguyên, giao diện của nó có khả năng cho ngƣời sử dụng đặt vào và lấy ra dữ liệu từ nó. Ta có thể biểu diễn giao diện này nhƣ sau: IBuff = <buff: seq(int), {put(in x: int), get(out y: int)}> ở đây seq(int) là kiểu dãy hữu hạn có thứ tự của các số nguyên và chúng ta qui ƣớc có thể dùng các ký pháp chuẩn để chỉ độ dài, phần tử đầu tiên hay cuối cùng của dãy. Định nghĩa (tính gộp lại): Hai Interface là có khả năng gộp lại (composable) nếu chúng không sử dụng cùng một tên trường với các kiểu khác nhau. Giả sử I và J là các Interface có khả năng gộp lại, kí pháp I ⊕ J biểu diễn một interface với các thành phần trường và phương thức như sau: (I ⊕ J).FDec def I. FDec ∪ J.FDec (I ⊕ J).MDec def I.MDec1 ∪ J.MDec Theo định nghĩa trên ta có các tính chất sau với các Interface có tính gộp lại: (1) I ⊕ I = I (2) I⊕ J = J⊕ I (3) I1⊕ (I2⊕ I3 ) = (I1⊕ I2)⊕ I3 Ta có thể dễ dàng chứng minh các tính chất này nhƣ sau: (1) Theo tính chất lũy đẳng của các phép toán tập hợp. (2) Theo tính chất giao hoán của các phép toán tập hợp. (3) Theo tính chất kết hợp của các phép toán tập hợp. Sự kế thừa interface: Kế thừa (inheritance) là các phƣơng tiện có ích cho sử dụng lại và lập trình gia tăng. Khi thành phần cung cấp chỉ một nhiệm vụ của các dịch vụ cần thiết hoặc một số phép toán đƣợc cung cấp là không đủ phù hợp cho sự cần thiết, chúng ta có thể sử dụng thành phần này bằng cách viết lại một số phép toán hoặc mở rộng nó với một số phép toán xử lý và các thuộc tính. Định nghĩa (kế thừa Interface): Cho I và J là các Interface, giả thiết rằng không có trường nào của J được định nghĩa lại trong I. Ký pháp I extends J biểu diễn một Interface có các miền trường và phương thức như sau: (I extends J).FDec def I.FDec ∪ J.FDec (I extends J).MDec def I.MDec ∪ {m(in: U, out: V)|m ∈ J.MDec∧ op ∉ I.MDec} Theo định nghĩa này, ta có các tính chất sau: (1) I extends (J1⊕ J2 ) = (I extends J1)⊕ (I extends J2) (2) (I1⊕ I2 ) extends J = (I1 extends J)⊕ (I2 extends J) Ta có thể chứng minh các tính chất này nhƣ sau: Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên Nguyễn Mạnh Đức Tạp chí KHOA HỌC & CÔNG NGHỆ 78(02): 97 - 104 99 (1) Theo tính chất kết hợp của các phép toán tập hợp và do (U \ V1 ) ∪ (U \ V2) = U \ (V1 ∪ V2) (2) Theo tính chất kết hợp của các phép toán tập hợp và do (U1 \ V ) ∪ (U2 \ V) = (U1 ∪ U2) \ V Sự làm ẩn (hiding): Để có thể đƣa ra các dịch vụ khác nhau cho các khách hàng khác nhau của một thành phần, chúng ta cho phép làm ẩn các phép toán trong một interface để không nhìn thấy chúng khi một thành phần đƣợc bao bởi các thành phần nào đó. Việc làm ẩn các toán tử cung cấp hiệu ứng ngƣợc với kế thừa giao diện và đƣợc sử dụng để giới hạn giao diện. Trong ký pháp đồ họa nhƣ UML, vấn đề này có thể thực hiện đƣợc bằng ký pháp tổng quát hóa [3, 9]. Định nghĩa (sự làm ẩn|sự che dấu): Giả sử I là interface và S là tập các tên phương thức. Ký pháp I\S chỉ interface I sau khi loại bỏ các phương thức của S từ phần khai báo phương thức của nó: (I\S).FDec def I.FDec (I\S).MDec def I.MDec \ S Việc làm ẩn các phép toán có các tính chất sau: (1) (I \ S1) \ S2 = I \ (S1 ∪ S2) (2) I \ ∅ = I (3) (I1 ⊕ I2) \ S = (I1 \ S) ⊕ (I2 \ S) (4) (I extends J) \ S = (I \ S) extends (J \ S) Chứng minh: giả sử U, U1, U2, V, V1, V2 là các tập hợp, ta có: (1) đƣợc thỏa mãn do (U \ V1 ) \ V2 = U \ (V1 ∪ V2) (2) đƣợc thỏa mãn do U \ ∅ = U (3) đƣợc thỏa mãn do (U1 ∪ U2) \ V = (U1 \ V) ∪ (U2 \ V) (4) đƣợc thỏa mãn do (U1 ∪ (U2 \ U1)) \ V = ((U1 \ V) ∪ (U2 \ V)) \ (U1 \ V). Từ (1) cho thấy rằng thứ tự của các phép toán trong 2 tập không quan trọng. Từ (3) ta thấy sự làm ẩn có tính phân phối với các toán hạng trong interface. Dựa vào các tính chất trên, một số các tính toán làm mịn của contract và thành phần đã đƣợc xây dựng và thực hiện [7, 8, 9]. HỢP ĐỒNG (CONTRACT) Hợp đồng (Contract) là ngữ nghĩa đặc tả các chức năng cho Interface. Đó là sự giao ƣớc quan hệ của một giao diện tới một ứng dụng bằng mô hình dữ liệu (trừu tƣợng) có tính rõ ràng, cụ thể, mô tả các chức năng của các toán tử dịch vụ, các giao thức đặc trƣng, và bảo đảm các chất lƣợng yêu cầu khác của các dịch vụ tùy thuộc vào ứng dụng. Mô hình cũng cung cấp định nghĩa nhất quán giữa các khung nhìn và phƣơng thức kiểm tra tính nhất quán này. Sự liên quan có thể mở rộng theo chiều ngang bằng cách bổ sung nhiều hơn các dịch vụ, các tính chất để bảo đảm chất lƣợng dịch vụ [3]. Sự đặc tả một phƣơng thức của một Interface là thiết kế D = (, P) [1], ở đây : -  là tập của các biến (cùng với kiểu của chúng) đƣợc sử dụng bởi phƣơng thức chứa trong các tham biến vào và ra. - P là tân từ có dạng (p ⊢ R) def (ok ∧ p)  (ok’ ∧ R) đƣợc sử dụng để mô tả các hành vi của phƣơng thức. p là tiền điều kiện, trạng thái khởi tạo đƣợc chấp nhận là đúng để nhờ đó mà phƣơng thức đƣợc kích hoạt và đƣợc biểu diễn bởi tập {x | x ∈ ( \ {out})} của các biến. Tân từ R đƣợc gọi là hậu điều kiện, xác định quan hệ các trạng thái khởi đầu tới các trạng thái cuối cùng và đƣợc mô tả bởi tập {x’ | x ∈ ( \ {in})}. Thiết kế D1 đƣợc làm mịn bởi thiết kế D2 (ký hiệu là D1 ⊑ D2) nếu: ok, ok’, v, v’ • (D2 D1) Một cách hình thức, contract đƣợc định nghĩa nhƣ dƣới đây. Định nghĩa (contract): Contract là cặp Ctr = (I, Init, MSpec, Prot), trong đó: 1. I là một Interface. 2. Init là hàm xác định các giá trị khởi đầu cho các trường đã khai báo trong I.FDec. 3. MSpec là ánh xạ mỗi phương thức m(in: U, out: V) của I tới sự đặc tả của nó là thiết kế với tập alphabet α, ở đây: inα def {in} ∪ I.FDec, outα def {out’} ∪ I.FDec’, α = inα ∪ outα. Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên Nguyễn Mạnh Đức Tạp chí KHOA HỌC & CÔNG NGHỆ 78(02): 97 - 104 100 4. Prot được gọi là giao thức của Interface, đó là tập các dãy hữu hạn có thứ tự của các sự kiện gọi phương thức. Dãy hữu hạn này có dạng m1, m2, , mk. Ý nghĩa của contract là: 1. Nếu ngƣời sử dụng các thành phần tuân theo giao thức khi tƣơng tác với thành phần, thì sẽ không xuất hiện các trạng thái đình trệ cũng nhƣ sai lệch, và 2. Tại mọi thời điểm khi ngƣời sử dụng gọi phép toán trong giao thức, trạng thái thay đổi và trả lại giá trị sẽ phù hợp trạng thái đặc tả chức năng của phép toán. Với nhiều ứng dụng, các giao thức có thể đƣợc chỉ rõ bởi các biểu thức chuẩn mực và trong trƣờng hợp thuận tiện có thể đƣợc kiểm tra tự động [3]. Ví dụ 2: Với giao diện của bộ đệm các số nguyên trong ví dụ 1, Một contract CtrBuff với giao diện của bộ đệm này có thể xác định nhƣ sau: CtrBuff.IBuff = IBuff // xác định như trong ví dụ 1 CtrBuff.Init = |buff| = 0 CtrBuff.MSpec(put(in x: int)) def (true ⊢ buff’ = ) CtrBuff.MSpec(get(out y: int)) def (true ⊢ buff =  out’ = head(buff)) CtrBuff.Prot = (put; get)* + (put; (get; put)*) Định nghĩa (reactive contract): Một contract tác động trở lại (reactive contract) là bộ ba Ctr = (I, Init, MSpec), ở đây MSpec gắn mỗi phép toán m(x, y) trong interface I với một thiết kế bị chặn. Ví dụ 3: Con tract trong ví dụ 2 có thể coi nhƣ contract tác động lại nhƣ sau: CtrBuff.I = IBuff // xác định như trong ví dụ 2 CtrBuff.Init = |buff| = 0 CtrBuff.MSpec(put(in x: int)) def (|buff| = 0) & (true ⊢ buff’ = ) CtrBuff.MSpec(get(out y: int)) def (|buff| > 0) & (true ⊢ buff’ =  y’ = head(buff)) Cho contract tác động lại Ctr = (I, Init, MSpec), hành vi động của nó đƣợc xác định bởi các tập các trạng thái không phù hợp và sai lệch F(Ctr) và D(Ctr). Mỗi phƣơng thức gọi m(u, v) bao gồm hai sự kiện ?m(u) để tiếp nhận yêu cầu và m(v)! để gửi trả lại cho lời gọi, cho nên mỗi vết của các trạng thái không phù hợp và sai lệch có dạng: ?m1(u1), m1(v1)!, , ?mn(un), mn(vn)! và ?m1(u1), m1(v1)!, , ?mn(un) Các trạng thái không phù hợp và sai lệch đƣợc xác định nhƣ sau [6]:  D(Ctr) bao gồm các dãy có thứ tự của các tƣơng tác giữa Ctr và môi trƣờng của nó dẫn contract tới trạng thái sai lệch.  F(Ctr) là tập của các cặp (s, X), ở đây s là dãy thứ tự của các tƣơng tác giữa Ctr và môi trƣờng của nó, X là tập các phƣơng thức để contract có thể từ chối trả lời sau khi thực hiện s. Một trạng thái không phù hợp (s, X) sẽ là một trong các trƣờng hợp sau đây: 1. s = và ∀m ∈ X . ךgm, k ≥ 0, nếu k=0 thì s = . Điều này tƣơng ứng với trƣờng hợp khi hệ thống tới trạng thái ở đó không bị chặn bởi của các sự kiện trong X là phù hợp, sau khi gọi thực hiện dãy có thứ tự này. 2. s = và mk! ∉ X. Điều này tƣơng ứng với trƣờng hợp khi phép toán mk đang đợi tới đầu ra kết quả của nó, biểu diễn bất kỳ của các phép toán khác sẽ có kết quả trong trạng thái không phù hợp. Vì nó cho rằng sự thi hành của phƣơng thức là nguyên tử. 3. s = và X có thể là tập bất kỳ của các phƣơng thức, ở đây sự thực hiện mk đƣa tới trạng thái đợi. 4. s ∈ D(Ctr) và X có thể là tập bất kỳ của các phƣơng thức. Đó là vết sai lệch với tập bất kỳ của các phƣơng thức luôn luôn là trạng thái không phù hợp. Ví dụ 4: Tiếp theo ví dụ trên, hành vi động của bộ đệm có thể đƣợc mô tả theo mô hình D/F ở trên nhƣ sau: D(CtrBuff) = 0 Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên Nguyễn Mạnh Đức Tạp chí KHOA HỌC & CÔNG NGHỆ 78(02): 97 - 104 101 F(CtrBuff) = {(s, X)  {?put, put!, ?get, get!}*  ℙ{?put, put!, ?get, get!}| (k  ℕ • s =  X  {?get, get!, put!}) (k  ℕ • s =  X  {?get, get!, put!}) (k  ℕ • s = <S(k), ?put(xk+1), put()!>  X  { get!, ?put, put!}) (k  ℕ • s =  X  { ?put, put, ?get!})} Ở đây: - ℙ{S} là một tập con của tập S. - S(k) def ?put(x1), put()!, ?get(), get(x1)!, , ?put(xk), put()!, ?get(), get(xk)! Chú ý rằng, khái niệm của các contract trong giới hạn chức năng tĩnh và các giao thức tƣơng tác đƣợc sử dụng để hỗ trợ cho việc lắp ghép các thành phần, khái niệm contract tác động trở lại đƣợc sử dụng để thiết kế, thẩm tra và cấp sự chứng nhận (chứng thực) [3]. Contract gộp lại: Hai contract có thể đƣợc gộp lại để mở rộng chúng chỉ khi các Interface của chúng có khả năng gộp lại, và những sự đặc tả của các phƣơng thức chung là nhƣ nhau (nhất quán). Thành phần kết cấu này sẽ đƣợc sử dụng để tính toán các dịch vụ cung cấp và yêu cầu khi các thành phần đƣợc bao gộp lại. Định nghĩa (composable Contract): Các Contracti = (Ii , Initi, MSpeci, Proti),với i =1, 2 có khả năng gộp lại nếu: 1. I1 và I2 có khả năng gộp lại và 2. Với bất kỳ phương thức m nào đang xuất hiện trong cả I1 và I2 MSpec1(m(in1: U, out1: V)) = MSpec2(m(u: U, v: V))[in1, out1’/u, v’] Trong trường hợp này contract gộp lại được ký pháp là Ctr1||Ctr2 và thành phần cấu trúc của nó được xác định bởi: I def (I1 ⊕ I2) và MSpec def MSpec1 ⊕ MSpec2 ở đây MSpec1 ⊕ MSpec2 chỉ sự ghi đè MSpec1(m) bằng MSpec2(m) nếu m xuất hiện trong cả I1 và I2. Chú ý mục đích của lập luận thành phần cấu trúc trên, điều kiện 2 tạo nên sự mở rộng bảo toàn thành phần cấu trúc này và các dịch vụ đƣợc giới hạn nhƣ dạng tổng quát hóa của ngôn ngữ mô hình hóa thống nhất UML [3]. Làm mịn Contract: Khái niệm làm mịn sau sẽ cho phép chúng ta so sánh và thay thế các thành phần tùy theo các contract của chúng. Định nghĩa (làm mịn contract): Cho Ctr1 và Ctr2 là các contract. Ctr1 được goi là làm mịn bởi Ctr2, ký hiệu là Ctr1 ⊑ Ctr2 nếu: 1. Ctr1.MDec ⊆ Ctr2.MDec 2. D(Ctr1) ⊇ D(Ctr2) 3. F(Ctr1) ⊇ F(Ctr2). Trong đó F(Ctr) là D(Ctr) là các tập đặc trƣng cho các hành vi động của các contract Ctr. Điều kiện 1 chỉ ra rằng Ctr2 cung cấp các dịch vụ không ít hơn của Ctr1, điều kiện 2 chỉ ra là Ctr2 không có khả năng sai lệch hơn Ctr1 và điều kiện 3 cho thấy rằng Ctr2 không có khả năng đình trệ hơn Ctr1 [3]. Contract tổng quát (General Contract): Contact tổng quát GCtr là mở rộng của khái niệm contract Ctr với việc khai báo một tập phương thức riêng PriMDec và sự đặc tả PriMSpect của chúng, GCtr = (Ctr, PriMdec, PriMSpec). Hành vi của GCtr được xác định trong Ctr. Một contract Ctr có thể xem nhƣ là contract tổng quát GCtr với PriMDec = . Làm ẩn dịch vụ (server hiding) của contract: Có thể làm ẩn phép toán chung trong MDec của contract tổng quát. Cho GCtr = (Ctr, PriMDec, PriMSpec) là một contract tổng quát, S là tập con của tập các phương thức chung MDec, thì GCtr\S là một contract được xác định như sau: (Ctr\S, PriMDec  S, PriMSpec  MSpec\S). Sự hợp thành của các contract: Cho GCtri, i = 1, 2 là 2 contract tổng quát thỏa mãn: 1. Tất cả các trƣờng chia sẻ chung có kiểu giống nhau; 2. Tất cả các phƣơng thức chia sẻ chung đƣợc đặc tả nhƣ nhau; 3. Điều kiện khởi tạo của hai contract là nhƣ nhau; Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên Nguyễn Mạnh Đức Tạp chí KHOA HỌC & CÔNG NGHỆ 78(02): 97 - 104 102 Sự hợp thành của các contract GCtr1 và GCtr2 là một contract tổng quát đƣợc ký hiệu là GCtr1||GCtr2 = ((I, Init, MSPec), PriMDec, PriMSpec), với: (GCtr1||GCtr2).I.FDec def GCtr1.I.FDec ∪ GCtr2.I.FDec (GCtr1||GCtr2).Init def GCtr1.Init  GCtr2.Init (GCtr1||GCtr2).I.MDec def GCtr1.I.MDEc ∪ GCtr2.I.MDec (GCtr1||GCtr2).MSpec def GCtr1.MSpec ⊕ GCtr2.MSpec (GCtr1||GCtr2).PriMDec def GCtr1.PriMDec ∪ GCtr2.PriMDec (GCtr1||GCtr2).PriMSpec def GCtr1.PriMSDec ⊕ GCtr2.PriMSDec THÀNH PHẦN (COMPONENT) Một thành phần là một sự thực thi của Contract với Interface đƣợc cung cấp của nó. Để thi hành một Contact, thành phần này có thể sử dụng các dịch vụ đƣợc cung cấp bởi các thành phần khác. Các dịch vụ đó đƣợc gọi là dịch vụ yêu cầu và đƣợc mô hình hóa nhƣ là một Contract của một Interface, Interface đó đƣợc gọi là Interface yêu cầu. Định nghĩa thành phần (component): Component C là bộ C = (I, Init, MCode, PriMDec, PriMCode, InMDec) ở đây: 1. I là một Interface, Init là điều kiện khởi đầu của nó. 2. PriMDec là tập các phương thức được khai báo ở miềm private trong component. 3. MCode (hoặc PriMCode) là ánh xạ mỗi phương thức m trong I.MDec (hoặc PriMDec) tới lệnh g&c bị chặn trong một ngôn ngữ lập trình. 4. InMDec chỉ ra Interface yêu cầu mà các phép toán của nó được gọi thực hiện từ các phép toán trong PriMCode và I.MDec, nhưng không được định nghĩa trong I.MDec ∪ PriMDec. Ta sử dụng C.I, C.Init, C.MCode, C.PriMDec, C.PriMCode, C.InMDec để chỉ các phần của một thành phần C. Chú ý: 1. Nhƣ đã trình bầy ở trên, mô hình của contract đƣợc sử dụng nhƣ là ngữ nghĩa chung cho các ngôn ngữ lập trình khác nhau dùng làm phƣơng tiện cho các thành phần. Điều đó tại sao nói rằng mô hình thành phần hỗ trợ khả năng cùng hoạt động. Đối tƣợng rCOS trong [2] cung cấp các tính toán thống nhất cho việc định nghĩa và suy luận cho cả ngôn ngữ lệnh và hƣớng đối tƣợng, và do đó có thể sử dụng để xây dựng hình thức các thành phần [6]. 2. Mô hình thành phần cũng hỗ trợ sự đóng gói của cả dữ liệu và sự thực hiện của các thành phần. Một thành phần có thể chỉ đƣợc sử dụng tùy theo contract của nó, đó là ngữ nghĩa trừu tƣợng của thành phần. Những sự hỗ trợ mạnh mẽ tính sử dụng lại này không chỉ với các thành phần, mà còn kiểm chứng các tính chất của các contract. Đó là điều cốt yếu của phƣơng pháp này [6]. Ngữ nghĩa của thành phần ở chức năng mà nó đƣa ra contract cho giao diện yêu cầu, trả về contract chung đƣợc tính toán từ mã của các phép toán. Các ngữ nghĩa của thành phần có thể xác định một cách hình thức nhƣ sau: Giả sử InCtr là một contract mà các phƣơng thức giao diện của nó giống nhƣ các phƣơng thức yêu cầu của thành phần C, nghĩa là InCtr.MDec = C.InMDec. Hành vi C(InCtr) của thành phần C đối với InCtr là một contract tổng quát ((I, MSpec), Init, PriMDec, PriMSpec), trong đó: I.FDec def C.FDec  InCtr.FDec I.MDec def C.MDec  InCtr.MDec Init def C.Init  InCtr.Init MSpec def  \ MDec PriMSpec def  \ PriMDec Ở đây  gán mỗi phép toán trong MDEc  PriMDec đƣơc tính toán thiết kế bị chặn từ mã (op) def guard(op)&[body(op)], nếu m  InMDec đƣợc gọi trong body(op), một sự Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên Nguyễn Mạnh Đức Tạp chí KHOA HỌC & CÔNG NGHỆ 78(02): 97 - 104 103 đặc tả của op gán bởi InCtr và đƣợc sử dụng trong tính toán [3]. Định nghĩa (làm mịn component): Một component C1 được làm mịn bởi component C2 ký hiệu là C1 ⊑ C2, nếu C1.MDec ⊆ C2.MDec, C1.InMDec⊇ C2.InMDec và sự làm mịn contract C1(InCtr) ⊑ C2(InCtr) thỏa tất cả các contract vào InCtr. Công nghệ thành phần còn hỗ trợ trên môi trƣờng nhiều lớp , cho phép một ƣ́ng dụng đƣợc chia nhỏ thành nhiều dịch vụ khác nhau chạy trên những hệ thống máy tính khác nhau. Một số dịch vụ nhƣ : lôgíc ƣ́ng dụng , thu thập thông tin , điều khiển giao dịch , hiển thị dữ liệu , và quản trị có thể chạy trên các máy tính khác nhau và giao tiếp để cung cấp cho ngƣời sƣ̉ dụng cuối một giao diện ƣ́ng dụng thống nhất. Sự hợp thành của các thành phần với nhau: Cho C1 và C2 là các thành phần mà chúng có miền các trƣờng và miền các phƣơng thức khác nhau, sự lắp ghép C1 với C2 sẽ hợp thành một contract mới (ký hiệu là C1 >> C2), với: (C1 >> C2).FDec def C1.FDec ∪ C2.FDec (C1 >> C2).MDec def C1.MDec ∪ C2.MDec (C1 >> C2).Init def C1.Init ∧ C2.Init (C1 >> C2).MCode def C1.MCode ∪ C2.MCode (C1 >> C2).PriMDec def C1.PriMDec ∪ C2.PriMDec (C1 >> C2).PriMCode def C1.PriMCode ∪ C2.PriMCode (C1 >> C2).InMDec def (C2.InMDec \ C1.MDec) ∪ C1.InMDec) Dễ thấy rằng toán tử lắp ghép là đơn điệu đối với sự làm mịn có thứ tự của các thành phần [3], Trong trƣờng hợp đặc biệt khi mà: (C1.InMDec ∪ C2.InMDec)  (C1.MDec ∪ C2.MDec) = ∅, thì phép lắp ghép C1 và C2 đƣợc gọi là phép hợp tách rời (disjoint union) và kí hiệu là C1||C2. Thành phần phản hồi (feedback component): Cho C là một thành phần, giả sử rằng phƣơng thức chung m của nó có cùng một số lƣợng và các kiểu của các tham số với phƣơng thức n đã đƣợc nhập vào. Ta sử dụng ký pháp C[m ↳ n] để biểu diễn một thành phần mà các việc phản hồi do dịch vụ đƣợc cung cấp m cho dịch vụ nhập vào n, với các phần nhƣ sau: C[m ↳ n].I def C.I \ {m} C[m ↳ n].Init def C.Init C[m ↳ n].MCode def (C.MDec) \ {m} ⊳ C.MCode C[m ↳ n].PriMDec def C.PriMDec ∪ {m} C[m ↳ n].PriMCode def C.PriMCode ∪ {m → C.MCode(m)} C[m ↳ n].InMDec def C.InMDec \ {n} Ví dụ 5: Ta định nghĩa 2 thành phần bộ đệm của các số nguyên C1 và C2 nhƣ sau: C1.FDec = {x1: seq(int)} C1.MDec = {put(in: int;), get1(; out: int)} C1.MCode(put) = (x1 := )⊳(x1 = < >)⊲(put1(head(x1);); x1 := ) C1.MCode(get1) = (x ≠ ) → (out := head(x1); x1 = ) C1.InMDec = {put1(in: int;)} C2.FDec = {x2: seq(int)} C2.MDec = {put1(in: int;), get(; out: int)} C2.MCode(put1) = (x2 = ) → (x2 = ) C2.MCode(get) = (out := head(x2); x2 := < >)⊳(x2 ≠ )⊲(get1(; out)) C2.InMDec = {get1(in: int;)} Do đó, C1 >> C2 đƣợc minh họa trên hình 1, (C1 >> C2) \ {get1) đƣợc minh họa trên hình 2 và C1>>C2)[C2.put1 ↳ C1.put1] đƣợc minh họa trên hình 3. KẾT LUẬN Chúng tôi đã 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 mô hình phát triển phần mềm thành phần, đó là: giao diện, các hợp đồng, các giao thức tƣơng tác, các thành phần; những quan hệ và sự biến đổi của chúng; các tính toán làm mịn. Từ đó cho thấy ý nghĩa và sự cần thiết khi phát triển Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên Nguyễn Mạnh Đức Tạp chí KHOA HỌC & CÔNG NGHỆ 78(02): 97 - 104 104 phƣơng pháp hình thức trong kỹ nghệ phần mềm hƣớng thành phần. Đó là những cơ sở cho các tính toán làm mịn để xây dựng và phát triển các hệ thống thành phần và đối tƣợng trong các giai đoạn khác nhau của tiến trình phát triển hệ thống. Các tính toán làm mịn ở đây đƣợc phát triển dựa trên mô hình tính toán rCOS, bảo đảm sự đúng đắn và nhất quán trong quá trình biến đổi và phát triển. Trên cở sở của các tính toán này chúng tôi sẽ xây dựng các hệ thống ứng dụng theo phƣơng pháp hƣớng thành phần, bảo đảm hiệu quả cho việc quản lý độ phức tạp và sự biến đổi của hệ thống và tận dụng tối đa khả năng sử dụng lại các thành phần. Lời cảm ơn: Nghiên cứu này có sử dụng một số kết quả trong đề tài nghiên cứu B2010- TN03-23. Chúng tôi xin chân thành cảm ơn sự hỗ trợ quý báu với đề tài B2010-TN03-23. TÀI LIỆU THAM KHẢO [1]. C.A.R. Hoare and He Jifeng (1998), Unifying Theories of Programming, Prentice Hall. [2]. He Jifeng, Li Xiaoshan and Zhiming Liu (2005), rCOS: Refinement Calculus for Object Systems, Technical report UNU/IIST No.322, UNU/IIST: International Institute for software technology, the United Nations University, Macau. [3]. J. Hefeng, Li Xiaohan and Li and Zhiming Liu (2005), Component-Based software engineering- the need to link method and their theories, No.330, UNU/IIST: International Institute for software technology, the United Nations University, Macau. [4].He Jifeng, Zhiming Liu, Li Xiaohan (2005), Reactive Components, Technical report UNU/IIST No.327, UNU/IIST: International Institute for software technology, the United Nations University. [5].Zhiming Liu, He Jifeng, Li Xiaohan (2005), “rCOS: Refinement of Component and Object Systems”. Invited talk at 3rd International Symposium on Formal Methods for Component and Object Systems. [6].Xin Chen, He Jifeng, Zhiming Liu and Naijun Zhan (2007), “A Model Component-Based Programming”, In International Symposium on Fundamentals of Software Engineering, to appear in LNCS, Springer. [7].Zhenbang Chen, Zhiming Liu, Anders P. Ravn, Volker Stolz and Naijun Zhan (2007), Refneinement and verification in component based model driven design, Technical report UNU/IIST No.388, UNU/IIST: International Institute for software technology, the United Nations University, Macau. [8].Đặng Văn Đức, Nguyễn Văn Vỵ, Nguyễn Mạnh Đức (2008), “Một qui trình phát triển hệ thống phần mềm trên cơ sở mô hình rCOS”, Kỷ yếu Hội thảo khoa học Quốc gia lần thứ 3 - Nghiên cứu cơ bản và ứng dụng công nghệ thông tin (FAIR07), nhà xuất bản Khoa học và Kỹ thuật, tr. 184-201. [9].Nguyễn Mạnh Đức, Đặng Văn Đức (2006), “Về một cách tinh chế mô hình lớp UML”, Tạp chí Tin học và điều khiển học, Viện Khoa học và Công nghệ Việt nam, 22 (1) tr. 63-74. SUMMARY SOME THE CALCULATES AND REFINEMENTS WITH COMPONENTS Nguyen Manh Duc * Faculty of Math., Thainguyen University of Education In this article we are formal of the basic and important concepts for model of development component software, including interfaces, contracts, interaction protocols, components, component compositions and the relations among these notions, the calculates and refinements among theses. The specification and calculates and refinements implemented based on rCOS model, ensure corrects and consistent of systems. The works can implements in different stages of process software development. From that place shows meaning and need when formal development method for component-oriented software engineering. Key words: rCOS, design, Interface, Contract, Component, UML * Tel: 0915 564 249; Email: nmductn@yahoo.com Số hóa bởi Trung tâm Học liệu – Đại học Thái Nguyên