intTypePromotion=1
zunia.vn Tuyển sinh 2024 dành cho Gen-Z zunia.vn zunia.vn
ADSENSE

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

Chia sẻ: Hoang Son | Ngày: | Loại File: PDF | Số trang:8

37
lượt xem
2
download
 
  Download Vui lòng tải xuống để xem tài liệu đầy đủ

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.

Chủ đề:
Lưu

Nội dung Text: 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 =
ADSENSE

CÓ THỂ BẠN MUỐN DOWNLOAD

 

Đồng bộ tài khoản
2=>2