Phương pháp hình thức đặc tả hệ thống hướng đối tượng dựa trên mô hình rcos - Nguyễn Mạnh Đức

T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 95 PHƯƠNG PHÁP HÌNH THỨC ĐẶC TẢ HỆ THỐNG HƯỚNG ĐỐI TƯỢNG DỰA TRÊN MÔ HÌNH rCOS Nguyễn Mạnh Đức (Trường ĐH Sư phạm - ĐH Thái Nguyên)- Đặng Văn Đức (Viện Công nghệ thông tin - Viện KH&CN Việt Nam)- Nguyễn Văn Vỵ (Trường ĐH Công nghệ- ĐH Quốc gia Hà Nội) 1. Đặt vấn đề 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 [1, 4]. 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 cơ sở cho việc phát triển phần mềm hướng đối tượng. Bài báo này sẽ trình bày một qui trình làm mịn mô hình UML dựa trên lý thuyết lập trình thống nhất của Hoare và He [2], sử dụng vào việc xây dựng một cách đúng đắn các chương trình hướng đối tượng. Trong tiến trình phát triển thống nhất RUP (rational unified process) dựa trên ngôn ngữ UML (unified modeling language) [1, 4, 7], một số mô hình loại khác nhau của UML đã được sử dụng để biểu diễn các mô hình nghiệp vụ, mô hình phân tích, mô hình thiết kế và mô hình triển khai trong pha khác nhau để phát triển hệ thống. Thí dụ, biểu đồ ca sử dụng biểu diễn mô hình nghiệp vụ (khung nhìn nghiệp vụ), biểu đồ lớp biểu diễn mô hình phân tích (khung nhìn tĩnh), biểu đồ công tác và biểu đồ trạng thái biểu diễn hành vi (khung nhìn hành vi) RUP sử dụng đồng thời nhiều khung nhìn trong việc mô hình hoá hệ thống cho phép người phát triển có thể phân chia mô hình hệ thống thành một số khung nhìn khác nhau để làm trực quan và quản lý chúng theo những cách riêng. Mỗi khung nhìn đơn sẽ tập trung vào một khía cạnh riêng biệt ở một giai đoạn, để phân tích và hiểu rõ các đặc trưng khác nhau của mô hình hệ thống. Tuy nhiên, mô hình hệ thống với nhiều khung nhìn phải đối mặt với các khó khăn về sự khác nhau của nhiều khung nhìn ở những thời điểm khác nhau của tiến trình phát triển. Một số vấn đề đã được đặt ra cần giải quyết [12]: 1) Tính nhất quán ngang của mô hình: Nhiều khung nhìn khác nhau của các hệ con khác nhau trong một hệ thống đòi hỏi phải tương thích với nhau về cú pháp và ngữ nghĩa. 2) Tính nhất quán dọc của mô hình: Khi biến đổi và phát triển một mô hình qua các bước làm mịn, đòi hỏi các mô hình nhận được ở mỗi bước phải nhất quán và có ngữ nghĩa phù hợp với nhau; 3) Tính lần vết được của mô hình: Khi chuyển từ một mô hình của một khung nhìn này sang mô hình theo một khung nhìn khác, hay từ bước làm mịn này sang bước sau phải được chỉ dẫn cho phép lần ngược lại mô hình loại trước hay mô hình ở bước trước, cũng như có thể lần xuôi đến các mô hình của bước sau, và đảm bảo sự phù hợp giữa các mô hình đó. 4) Tích hợp được các mô hình: Mô hình của các khung nhìn khác nhau cần phải tích hợp đảm bảo sự nhất quán và đồng bộ toàn hệ thống trước khi có sản phNm phần mềm cuối cùng... Nhiều nghiên cứu về tính chất và hình thức thể hiện của các mô hình UML [10, 12] đã được tiến hành trong những năm gần đây. Tuy nhiên, phần lớn các nghiên cứu chỉ liên quan tới hình thức của từng loại biểu đồ riêng rẽ và tính nhất quán của các mô hình loại 1 hoặc loại 2. T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 96 Nhìn lại tiến trình phát triển hệ thống phần mềm theo hướng đối tượng theo RUP ta thấy, bắt đầu của tiến trình phát triển với khung nhìn nghiệp vụ, có chứa mô hình lớp khái niệm, và cho đến khi kết thúc tiến trình trước khi chuyển sang mã nguồn, chúng ta lại nhận được biểu đồ lớp thiết kế của hệ thống phần mềm. Nếu ta chỉ sử dụng một khung nhìn duy nhất được biểu diễn bằng các biểu đồ lớp, ta sẽ khắc phục được tính đa khung nhìn của tiến trình phát triển ở trên. Vấn đề duy nhất còn cần phải giải quyết ở đây là: làm sao xây dựng được các phép biến đổi và các quy tắc kiểm tra sự đúng đắn của chúng, khi đó bằng một loạt các phép biến đổi đúng đắn, ta có thể chuyển biểu đồ lớp khái niệm ban đầu thành biểu đồ lớp thiết kế cuối cùng của phần mềm hệ thống (hình vẽ dưới đây) [16, 17]. Lúc này, các khung nhìn khác của tiến trình RUP sẽ được sử dụng như các công cụ trợ giúp cho việc xác định các phép biến đổi cụ thể để tận dụng được thế mạnh của các khung nhìn này. Vấn đề cuối cùng đặt ra được giải quyết bằng công cụ hình thực hóa dựa trên các quan hệ đại số. Nhìn trến sơ đồ ta thấy, để đạt đến biểu đồ lớp thiết kê cuối cùng, chúng ta cần đến các phép biến đổi sau: thêm lớp (có thể kế thừa), thêm thuộc tính, thêm phương thức, thay đổi đặc trưng của thuộc tính, của phương thức, thay đổi liên kết giữa các lớp và các biến đổi tương ứng trong mỗi phương thức. 2. Cơ sở của các phép biến đổi Một biểu diễn của chương trình lệnh được coi như một thiết kế (design) xác định bởi cặp (α, P) [2, 3], ở đây α biểu thị tập các biến đã biết trong thiết kế, được gọi là bảng ký kiệu của thiết kế; P là các toán tử xác định quan hệ giữa các giá trị ban đầu của các biến và các giá trị kết quả của nó, ta ký hiệu quá trình biến đổi như sau: p(x) ├ R(x, x’), cụ thể hơn như sau: p(x) ├ R(x, x’) def ok ∧ p(x) ⇒ ok’∧ R(x, x’) Trong đó: p(x) được gọi là tiền điều kiện và phải có giá trị true – tức là đúng đắn trước khi chương trình bắt đầu. R(x, x’) gọi là hậu điều kiện nhận được sau khi chương trình thực hiện. x và x’ biểu diễn giá trị khởi đầu và kết thúc của biến x trong chương trình. ok và ok’ là các biến logic mô tả trạng thái hành vi ban đầu và cuối của chương trình: nếu chương trình được kích hoạt hợp thức ok là true, nếu việc thực hiện chương trình cuối cùng thành công ok’ là true, ngược lại chúng là false. biểu đồ lớp khái niệm miền lĩnh vực biểu đồ lớp thiết kế phần mềm hệ thống phép BĐ1 biểu đồ lớp được làm mịn 1 phép BĐ2 phép BĐn mô hình nghiệp vụ khung nhìn 1 mô hình phân tích khung nhìn 2 mô hình thiết kế khung nhìn k Ý tưởng cho phương pháp giải quyết vấn đề Tiến trình RUP Phương pháp mới T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 97 2.1. Mô tả hệ thống hướng đối tượng Một hệ thống hoặc chương trình hướng đối tượng S có dạng cdecls ● P , ở đây: cdecls là phần khai báo một số hữu hạn các lớp; P được gọi là phương thức chính và có dạng (glb, c), trong đó glb là tập hữu hạn các biến chung và kiểu dữ liệu của chúng, còn c là các lệnh. P có thể dược hiểu như là phương thức chính nếu S được tạo bởi ngôn ngữ giống như Java. Phần khai báo lớp cdecls là thứ tự của các khai báo lớp cdecl1; ...; cdeclk,. Ở đây mỗi khai báo lớp cdecli có dạng như sau: [private] class N [extends M] { pri : T1 t1 = a1 ..., Tm tm = am; pro : U1 u1 = b1 ..., Un un = bn; pub : V1 v1 = d1 ..., Vk vk = dk; meth : m1 (T11 x11, T12 y12, T13 z13) { c1 }; ... ; mℓ (Tℓ1 xℓ1, Tℓ2 yℓ2, Tℓ3 zℓ3) { cℓ } } trong đó: 1. Mỗi lớp có thể được khai báo private hoặc là public, ngầm định là public. Chỉ các lớp có kiểu public hoặc kiểu cơ sở mới được sử dụng trong các khai báo biến chung glb. 2. N và M là các tên lớp khác nhau và M được gọi là lớp cha của N. 3. Phần pri khai báo các thuộc tính private của lớp, bao gồm kiểu và các giá trị khởi tạo. Tương tự, các phần pro và pub khai báo các thuộc tính protected và public của lớp. 4. Phần method khai báo các phương thức của lớp N, trong đó m1, m2, ..., mℓ là các phương thức, ở đây (Ti1 xi1), (Ti2 yi2), (Ti3 zi3) và ci biểu diễn các tham biến giá trị, các tham biến kết quả, các tham biến giá trị kết quả và phần thân của phương thức mi. Phương thức có thể được chỉ ra bởi biểu diễn m(paras){c}, trong đó paras là các tham biến và c là thân lệnh của m. Khi viết các luật làm mịn, ký pháp sau được sử dụng để chỉ sự khai báo lớp N: N [M, pri, pro, pub, op]. Trong đó, M là tên lớp cha của N; pri, pro và pub là các tập thuộc tính private, protected và public của N; còn op là tập các phương thức của N. Ta có thể chỉ đưa ra các tham số liên quan cần thiết chẳng hạn như: nếu sử dụng N[op] để chỉ lớp N với tập các phương thức op, N[pro, op] chỉ lớp N với các thuộc tính protected là pro và tập các phương thức là op. 2.2. Mô tả biểu thức Biểu thức trong ngôn ngữ hướng đối tượng có thể xuất hiện vế bên phải của các lệnh gán, xác định theo các qui tắc như sau [2, 5]: e ::= x | null | self | e.a | e is C | C(e) | f(e) Trong đó x là biến đơn, null là kiểu đối tượng đặc biệt, lớp đặc biệt NULL là lớp con của mọi lớp và null là duy nhất, self được sử dụng để chỉ đối tượng hoạt động trong phạm vi hiện tại, e.a là thuộc tính a của e, e is C là kiểu kiểm thử (test), C(e) là biểu thức có kiểu theo khuôn mẫu, f(e) là phép toán gắn liền với các kiểu nguyên thuỷ. 2.3. Mô tả các lệnh Phần này xét các lệnh hỗ trợ việc xây dựng chương trình hướng đối tượng tiêu biểu [2, 5]. T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 98 c ::= skip | chaos | var T x = e | end x bỏ qua| không xác định khai báo | kết thúc khai báo c; c | c
bc | c ⊓ c | b*c tuần tự| chọn theo điều kiện| không tiền định| lặp le.m(e, v, u) | le:=e | C.new(x) gọi phương thức | gán| tạo đối tượng mới. Ở đây b là biểu thức logic, c là lệnh, e là một biểu thức, le có thể xuất hiện ở vế trái của phép gán và có dạng le ::= x|le.a với x là biến đơn còn a là thuộc tính của đối tượng. Đa số các lệnh có ý nghĩa tương tự như trong các ngôn ngữ lệnh (có thể xem chi tiết trong [2, 5]). Sau đây là các giải thích một số lệnh đặc trưng cho chương trình hướng đối tượng. Lệnh gán le := e được xác định đúng khi le và e đã được xác định đúng và kiểu của e là kiểu con của kiểu đã được khai báo le. Trong trường hợp lệnh gán đơn x := e, khi lệnh gán được xác định đúng nó chỉ thay đổi x bởi gán x bằng giá trị của e. Trong trường hợp sự thay đổi thuộc tính của đối tượng, le.a := e thay thuộc tính a của đối tượng le bằng giá trị e. Phương thức gọi le.m(e, v, vr) xác định đúng nếu le là đối tượng không rỗng và m(x, y, z) là phương thức đã được khai báo trong kiểu le. Khi nó đã được xác định đúng, việc thực hiện các lệnh gán các giá trị của các tham số thực v và vr cho các tham số hình thức x và z của m của các đối tượng hoạt động le tham chiếu tới, rồi thực hiện thân của phương thức trong môi trường của lớp đối tượng hoạt động. Sau khi thực hiện các thân cuối cùng, giá trị của tham biến kết quả và tham biến giá trị kết quả y và z được trả lại hợp qui cách với các tham số thực r và vr. Lệnh tạo đối tượng mới C.new(x) được xác định đúng nếu C là lớp đã được khai báo. Sự thực hiện lệnh này sẽ tạo ra một đối tượng mới của lớp C với biến tham chiếu là x và gắn giá trị khởi đầu của các thuộc tính trong lớp C với giá trị các thuộc tính của x. 3. Các phép biến đổi làm mịn mô hình hệ thống đối tượng 3.1. Các khái niệm Sau đây ta xem xét một số khái niệm liên quan tới quá trình làm mịn mô hình hệ thống [3, 9, 11, 13, 14]: Định nghĩa 1 (làm mịn thiết kế): Thiết kế D2 = (α, P2) là làm mịn của thiết kế D1=(α, P1) được ký hiệu là: D1 ⊑ D2, nếu P2 dẫn tới P1, nghĩa là: ∀x, x’, ..., z, z’, ok, ok’: (P2 ⇒ P1). Ở đây x, ..., z là các biến chứa trong α.. D1≡ D2 nếu và chỉ nếu D1⊑ D2 và D2 ⊑ D1. Định nghĩa 2 (làm mịn dữ liệu): Cho ρ là ánh xạ α2 tới α1. Thiết kế D2 = (α2, P2) là làm mịn của thiết kế D1 = (α1, P1) dưới ρ, được ký hiệu là D1⊑ρ D2, nếu (ρ; P1)⊑ (ρ;P2). Trong trường hợp này ρ được gọi là ánh xạ làm mịn. Định nghĩa 3 (làm mịn hệ thống): Cho S1 và S2 là các đối tượng chương trình có cùng một tập các biến chung glb. S2 là làm mịn của S1, được chỉ ra bởi S1 ⊑sys S2, nếu hành vi của nó có thể kiểm soát và dự đoán nhiều hơn trong S1, tức là: ∀ x, x’, ok, ok’: (S2⇒ S1) Ở đây x là các biến trong glb.Ý nghĩa này là hành vi mở rộng của S1, đó là các cặp tiền điều kiện và hậu điều kiện của các biến chung là tập con của S2. Để phạm vi của S1 và S2 được làm mịn là khác nhau, ta yêu cầu chúng phải có cùng tập các biến chung và tồn tại ánh xạ làm mịn từ các biến của S1 tới S2 trên tập các biến chung đó. Định nghĩa 4 (làm mịn lớp): Cho cdecls1 và cdecls2 là hai khai báo. cdecls2 là làm mịn của cdecls1, đượcký hiệu lài cdecls2 ⊒class cdecls1 nếu như phần trước có thể thay thế T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 99 phần sau trong bất kỳ hệ thống đối tượng: cdecls2 ⊒class cdecls1 def ∀P . (cdecls2• P ⊒sys cdecls1• P). Ở đây P đóng vai trò cho phương thức chính (glb, c). Phương thức chính tương ứng với chương trình ứng dụng đang sử dụng các dịch vụ Do đó, ở đây ta chỉ quan tâm làm mịn giữa các phần khai báo. 3.2. Xây dựng qui trình làm mịn mô hình Quá trình làm mịn được thực hiện theo các luật làm mịn đã được đã được xác định [3, 10, 11]. 3.2.1. Xây dựng hệ thống khởi tạo ban đầu Mô hình hệ thống khởi tạo ban đầu còn gọi là mô hình khái niệm thô, đó chính là mô hình lĩnh vực miềm, mô tả các khái niệm quan trọng của hệ thống qua các đối tượng của lĩnh vực nghiệp vụ và các liên kết giữa chúng với nhau. Thuật toán bổ sung các lớp vào mô hình khởi tạo: Công việc đầu tiên là tạo mô hình khởi tạo của hệ thống, cụ thể là bổ sung tên các lớp Ni đặc trưng cho các đối tượng miền lĩnh vực vào biểu đồ lớp của mô hình hệ thống có dạng: APP0 = N1[]; N2[]; ...; Nk[] và xác định những quan hệ giữa các Ni. Phép biến đổi này được thực hiện bằng thuật toán addClassName như sau: // Thuật toán addClassName- bổ sung các lớp vào mô hình Input: Một tên xâu cho định danh cho lớp Ni. Output: Lớp Ni trống (chưa có các thuộc tính hoặc phương thức). Format: addClassName () Method: var stop: Boolean, s: String; stop := false; while ¬ stop do { read(s); if {(s ””) → AdditionClassName(s)} fi; read(stop); } end stop, s; End. Ở đây, cấu trúc if {(bi → Pi) | 1 ≤ i ≤ n} fi là sự thực hiện liên tiếp có điều kiện. Trong đó, mỗi Pi được chọn để thực hiện nếu bi là true. Khi mọi bi là false thì kết quả là chaos [2]. Phep bổ sung lớp này sẽ được dùng cho việc bổ sung tiếp tục các lớp sau này vào hệ thống. 3.2.2. Xây dựng các biến đổi làm mịn mô hình khái niệm hệ thống [14, 16, 17] Thuật toán bổ sung các thuộc tính cho lớp: Khi đã có một lớp, ta cần xác định và bổ sung các thuộc tính private và định dạng các kiểu cho nó. (khi không giả thiết gì, thuộc tính trong lớp mặc định là private). Việc thêm một thuộc tính thành phần vào một lớp có thể được thực hiện theo luật bổ sung sau: Ni[]; cdecls ⊑ Ni[pri ]; cdecls T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 100 Trong đó T là một kiểu dữ liệu của thuộc tính attributeName và d là giá trị khởi đầu nếu cần. Với mỗi lớp, thực hiện nhiều lần luật này để bổ sung đầy đủ các thuộc tính cho nó. Quá trình này có thể được mô tả bẳng thuật toán hình thức như sau: // Thuật toán addAttributeName- bổ sung các thuộc tính vào lớp Input: Một lớp Ni của hệ thống, . Output: Lớp Ni bao gồm các thuộc tính kiểu private cần thiết. Format: addAttributeName () Method: var stop: Boolean, s: String; stop := false; while ¬ stop do { read(s); if {(s ””) → AdditionAttributeName(s)} fi; read(stop); } end stop, s; End. Thực hiện k lần thuật toán này để bổ sung các thuộc tính cho k lớp của hệ thống. Thuật toán chuyên đổi kiểu thuộc tính: Tiếp theo là chuyển các thuộc tính kiểu private cần thiết sang kiểu protected để được hỗ trợ các dịch vụ nhiều hơn. Muốn vậy, ta sẽ áp dụng luật chuyển đổi kiểu thuộc tính sau: Ni[pri ]; cdecls ⊑ Ni[pro ]; cdecls Việc chuyển thuộc tính kiểu private trong một lớp sang kiểu protected theo thuật toán sau: // Thuật toán priAttToproAtt, chuyển kiểu thuộc tính private thành protected Input: Một lớp khái niệm Ni của hệ thống ứng dụng. Output: Lớp Ni bao gồm các thuộc tính kiểu protected cần thiết. Format: priAttiToproAtt () Method: var stop: Boolean, ok: Boolean; stop := false; ok := false; while ¬ stop do { if {(type(Ni.AttributeName) = private) → { Question (ok); if {ok=true → priTopro(Ni.AttributeName)}fi; } fi; read(stop); } end stop, ok; End. T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 101 Bằng cách tương tự, ta cũng có thể xây dựng các thuật toán chuyển kiểu thuộc tính protected sang kiểu public. Sau mỗi bước thực hiện các công việc làm mịn trên sẽ thu được một mô hình thống mới và ta có: Mô hình khái niệm thô ⊑ Mô hình khái niệm mịn ban đầu. 3.2.3. Xây dựng mô hình thiết kế ban đầu cho hệ thống Thuật toán bổ sung các phương thức cho lớp: Mô hình thiết kế là mô hình gồm các lớp có chứa đầy đủ thuộc tính và phương thức. Bằng cách bổ sung các phương thức cho các lớp của mô hình khái niệm ta được mô hình thiết kế. Có thể áp dụng các luật bổ sung phương thức như sau: N[op]; cdecls ⊑ N[op ∪ m(paras) {c}]; cdecls Thuật toán bổ sung các phương thức vào một lớp có thể viết như sau: // Thuật toán addMethodName- bổ sung các phương thức vào lớp Input: Một lớp Ni của hệ thống ứng dụng. Output: Lớp Ni bao gồm các phương thức cần thiết. Format: addMethodName () Method: var stop: Boolean, s: String, paras: String; stop := false; while ¬ stop do { read(s, paras); if {(s ””) → AdditionMethodName(s, paras)} fi; read(stop); } end stop, s, paras; End. Sau phép biến đổi này ta có: Mô hình khái niệm mịn ⊑ Mô hình thiết kế ban đầu. 3.2.4. Làm mịn mô hình thiết kế hệ thống Các công việc trong phần này tuỳ thuộc nhiều vào bài toán nghiệp vụ cụ thể đặt ra. Trong bước này chúng ta có thể áp dụng nhiều luật làm mịn khác nhau để làm mịn dần hệ thống từ mô hình thô về dạng sát với mã trình có thể thực hiện được, tạo điều kiện thuận lợi cho quá trình dịch xuôi từ mô hình UML sang một ngôn ngữ hướng đối tượng mà nó hỗ trợ. Ở đây cần thực hiện các luật khác nhau để làm mịn dần cho hệ thống với các thao tác biến đổi sau đây [3, 11]: - Làm mịn các phần thân phương thức m(){c} trong các lớp: Áp dụng luật Extract Method, Move Method, Add Parameter - Chuyển thuộc tính từ một lớp tới lớp khác: Ápdụng luật Move Field [11], để chuyển thuộc tính từ một lớp sang lớp khác như sau: cdecl; M[b: N, a: T, op]; N[] ⊒ cdecls; M[b: N, op]; N[a: T] - Xây dựng các thừa kế cho các lớp: Áp dụng các luật tạo quan hệ giữa các lớp, chế tác lại định hướng mẫu, như Decorator, Strategy, luật thay thế điều kiện bằng tính đa hình ... T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 102 Với mỗi hệ thống ứng dụng cụ thể, ta có thể linh hoạt áp dụng các luật làm mịn khác nhau đã trình bày ở trên để biến đổi dần hệ thống cho bài toán đặt ra. Khi kết thúc các phép biến đổi, ta sẽ có một hệ thống bao gồm các lớp thiết kế với đầy đủ thuộc tính và phương thức. Do quá trình biến đổi thực hiện đảm bảo tính đúng đắng, nhất quán và phù hợp, nên hệ thống nhận được ở dạng hình thức hóa đặc tả đúng đắn những gì ta mong muốn về hệ thống cần xây dựng. 4. Kết luận Bài báo đã trình bầy một tiến qui trình phát triển hệ thống phần mềm hướng đối tượng trên cơ sở các luật và các thuật toán biến đổi làm mịn, chúng được xây dựng dựa trên tính đúng của luật làm mịn và tính đúng của đặc tả hình thức đã xét. Để thực hiện các biến đổi làm mịn, các thuật toán làm mịn tương ứng được xây dựng phục vụ cho việc phát triển các mô hình hệ thống từ khái niệm đến thiết kế để được mô hình thiết kế cuối cùng đặc tả hệ thống cần xây dựng. Chúng tôi đã xây dựng các thuật toán: addClassName, addAttributeName, MoveAtt, priAttToproAtt, proAttTopubAtt, MoveMethod, addMethodName, RelationShip, Inheritance1, Inheritance2, Polymorphism để phục vụ cho đặc tả quá trình làm mịn và tinh chế các hệ thống hướng đối tượng [15, 16, 17]. Qua quá trình làm mịn cho ta mô hình thiết kế cuối cùng có biểu diễn tương đối gần với chương trình ở dạng ngôn ngữ lập trình có thể thực hiện được. Điều đó làm dễ dàng cho việc cài đặt hệ thống bằng bất kỳ ngôn ngữ lập trình hướng đối tượng, chẳng hạn như C#.Net hay Java. Để áp dụng được các bước làm mịn cụ thể đối với mỗi bài toán, việc sử dụng các khung nhìn của tiến trình RUP là rất cần thiết. Nó là những những mô hình trực quan, cho ta những gợi ý cho việc lựa chọn các phép biến đổi cần thiết ở mỗi bước. Khi thực hiện các phép biến đổi này, ở đây mới nêu ra được các việc cần làm để được hệ thống cuối cùng. Tuy nhiên, mô hình thiết kế tối ưu hay không chưa được đề cập. Ngoài ra, thực sự chúng tôi mới đưa ra nhưng phép biến đổi cơ bản. Còn có nhiều phép biến đổi liên quan đến những trường hợp tinh tế cũng chưa đề cập đến. Đó chính là những vấn đề đặt ra cần được tiếp tục nghiên cứu để có được một sự hoàn thiện và khả năng triển khai hiệu quả cao
Tóm tắt Trong bài báo này trình bày những nghiên cứu bước đầu về một tiến trình hình thức để đặc tả quá trình phát triển một hệ thống hướng đối tượng. Xuất phát từ biểu đồ miền lĩnh vực nghiệp vụ, quá trình phát triển hệ thống dựa trên tiến trình RUP nhưng được thực hiện bằng các biến đổi hình thức trên cơ sở các quan hệ đại số và các luật để đảm bảo tính đúng đắn của kết quả nhận được. Các phép biến đổi bao gồm thêm lớp, thêm thuộc tính, các phương thức cho lớp, phát triển các lớp kế thừa, chuyển đổi đặc trưng các thuộc tính của lớp, chuyển thuộc tính và toán tử từ một lớp sang một lớp khác, các phép toán đặc tả một phương thức của một lớp... Kết quả nhận được sẽ là một đặc tả hình thức của hệ thống với các lớp với các thành phần của nó. Do sự đặc tả trực quan gần với mô hình UML và ngôn ngữ lệnh nên có chuyển kết quả cuối cùng sang biểu đồ thiết kế với các lớp bằng UML, từ đó sử dụng Rational Rose để chuyển thành mã lệnh. Key words: UML, RUP, Rational Rose, Object–Oriented, refinement, process, class, attribute, operation T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 103 Summary The formal method specsification Object-Oriented System base on relation model This paper presents a algebric relations – based formal refinement process for the object- oriented software system development. Starting at the conceptual class model of one applied domain (in conjunction with RUP), the refinement process trasforms this model to the final design class model by sequent applying number of algebric relations-based formal transformations and relevant rules. Theses transformations include these adding classes to the exsiting system model, adding and changing attrributes, operations in the clasess of this model, and also instructions in the operations of one class... The final design class model is a design specificaton of the expected software system. The repesentation of this final model is closed to one of the object-oriented programming languages. Tài liệu tham khảo [1] Booch, G., Rumbaugh, J. and Jacobson, I., The Unified Modeling Language User Guide, Addison- Wesley, 1999. [2] C.A.R. Hoare and He Jifeng, Unifying Theories of Programming, Prentice Hall, 1998. [3] He Jifeng, Li Xiaohan and Zhiming Liu, rCOS: Refinement Calculus for Object Systems, Technical report UNU/IIST No.322, UNU/IIST: International Institute for software technology, the United Nations University, Macau, May 2005. [4] Ivar Jacopson, Gray Booch and James Rumbaugh, The Unified Software Development Process, Addision-Wesley, 2000. [5] J. He, Z. Liu, X. Li and S.Qin, A relational model for object-oriented designs. In Pro APLA’2004 LNCS 3302, Taiwan, 2004, Springer. [6] Joshua Kerievsky, Refactoring to patterns, Addison-Wesley, 2004 [7] Kuchten P., The Rational Unified Process – An Introduction, Addison-Wesley, 2000. [8] Larman, Applying UML and patterns, Prentice-Hall International, 2001. [9] Martin Fowler, Refactoring, improving the design of existing code, Addison-Wesley, 2000. [10] R.J.R. Back, L. Petre and I.P. Paltor, Formalizing UML use cases in the refinement calculus. In Proc. UML’99. Springer-Verlag, 1999. [11] Quan Long, He Jifeng, Zhiming Liu, Refactoring and pattern-directed refactoring: A formal perspective, Technical report UNU/IIST No.318, UNU/IIST: International Institute for software technology, the United Nations University, Macau, January 2005. [12] P. Andre, A. Romanczuk, J.C. Royer and A. Vasconcelos, Checking the consistency of UML class diagrams using Larch Prove. In Proc. ROOM’2000, York, UK, 2000. [13] Nguyễn Mạnh Đức, Nguyễn Văn Vỵ, Đặng Văn Đức (2005), “Mô hình đại số quan hệ của hệ thống hướng đối tượng”, 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, 21 (3) tr.261-270. [14] 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. [15] Nguyễn Mạnh Đức, Đặng Văn Đức (2006), “Ứng dụng phương pháp hướng đối tượng và ngôn ngữ UML mô hình hoá hệ thống E-Learning”, Tạp chí Khoa học và Công nghệ, Viện Khoa học và Công nghệ Việt Nam, 44 (3) tr. 33-42. [16] Nguyễn Mạnh Đức (2007), Thiết kế hướng đối tượng và xây dựng hệ thống thông tin phức tạp, Luận án Tiến sĩ Toán học, Viện Công nghệ Thông tin - Viện KH&CN Việt Nam. [17] Đặng Văn Đức, Nguyễn Văn Vỵ, Nguyễn Mạnh Đức (2007), “Một số thuật toán tinh chế cấu trúc hệ thống hướng đối tượng dựa trên các luật làm mịn của rCOS”, Kỷ yếu 30 năm thành lập Viện Công nghệ Thông tin, Viện Công nghệ Thông tin - Viện KH&CN Việt Nam.