Một cách đặc tả thiết kế hướng đối tượng dựa trên mô hình rCOS

T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br /> MỘT CÁCH ĐẶC TẢ THIẾT KẾ HƯỚNG ĐỐI TƯỢNG<br /> DỰA TRÊN MÔ HÌNH rCOS<br /> Nguyễn Mạnh Đức (Trường ĐH Sư phạm - ĐH Thái Nguyên)<br /> Đặng Văn Đức (Viện Công nghệ Thông tin-Viện KH&CN Việt Nam)<br /> <br /> 1. Đặt vấn đề<br /> Thiết kế và phát triển hệ thống phần<br /> mềm với ngôn ngữ hướng đối tượng đã<br /> được thừa nhận là rất phức tạp [1, 4]. Nhiều<br /> nhà nghiên cứu chỉ ra sự cần thiết phát triển<br /> công cụ hình thức hoá làm nền tảng cho<br /> việc phát triển phần mềm hướng đối tượng.<br /> Bài báo này sẽ giới thiệu lý thuyết lập trình<br /> thống nhất của Hoare và He [2] dùng vào<br /> việc xây dựng một cách đúng đắn các<br /> chương trình hướng đối tượng. Lý thuyết lập<br /> trình được vận dụng để trình bày ngữ nghĩa<br /> của ngôn ngữ lập trình hướng đối tượng với<br /> các lớp, tính rõ ràng, liên kết động, các<br /> phương thức đệ quy và tính đệ quy. Để cho<br /> đơn giản, những gì liên quan đến các định<br /> nghĩa hình thức về biến, tham chiếu tới các<br /> kiểu được bỏ qua (có thể xem trong [2, 5]).<br /> Phần 2 của bài báo là trình bày tóm tắt<br /> mô hình tính toán rCOS đã được He Jifeng<br /> và cộng sự đề xuất và phát triển [3]. Phần 3<br /> là đề xuất mới về việc áp dụng rCOS vào<br /> việc xây dựng một số đặc tả hệ thống phục<br /> vụ cho phát triển hệ thống phần mềm theo<br /> phương pháp hướng đối tượng.<br /> 2. Mô hình tính toán rCOS [3]<br /> Một chương trình lệnh được xác định<br /> bằng quan hệ nhị phân (α, P) [2, 5, 11],<br /> trong đó: α ký hiệu tập các biến đã biết<br /> trong chương trình. P là tân từ quan hệ các<br /> giá trị của các biến trong chương trình khi<br /> khởi tạo với các giá trị cuối của chúng, P<br /> còn được gọi là thiết kế (design).<br /> Với chương trình tuần tự lệnh, ta quan<br /> tâm theo dõi các giá trị của các biến vào inα và<br /> các biến ra outα. Ở đây ta đưa ra qui ước rằng<br /> với mỗi biến x ∈ inα, phiên bản x’ của nó là<br /> <br /> một biến ra trong outα, mang giá trị cuối của x sau<br /> khi thực hiện chương trình. Ta dùng biến logic ok<br /> chỉ ra một chương trình có khởi tạo đúng hay không<br /> và phiên bản ok’ của nó biểu diễn sự thực hiện có<br /> kết thúc hay không. Bảng ký tự α được định nghĩa<br /> là inα ∪ outα ∪ {ok, ok’} và thiết kế có dạng:<br /> p(x) ├ R(x, x’) def ok ∧ p(x) ⇒ ok’<br /> ∧ R(x, x’)<br /> Trong đó: p là tân từ trên inα và R là tân từ<br /> trên outα; p là tiền điều kiện, xác định trạng thái<br /> khởi đầu của chương trình; R là hậu điều kiện,<br /> xác định trạng thái kết thúc của chương trình; x<br /> và x’ biểu diễn giá trị khởi đầu và kết thúc của<br /> biến x trong chương trình; ok và ok’ tương ứng<br /> mô tả trạng thái ban đầu và cuối của chương trình,<br /> nếu chương trình được kích hoạt hợp thức ok là<br /> true, nếu việc thực hiện chương trình cuối cùng<br /> thành công ok’ là true, ngược lại chúng là false.<br /> 2.1. Thiết kế<br /> Một thiết kế biểu diễn sự thoả thuận giữa<br /> “người sử dụng” và chương trình, nếu chương<br /> trình được khởi tạo một cách hợp thức trong<br /> trạng thái thoả mãn tiền điều kiện p thì nó sẽ kết<br /> thúc trong trạng thái thoả mãn hậu điều kiện R.<br /> <br /> Một thiết kế V thường có dạng sau:<br /> V: (p├ R) def p ⊢ (R ∧ w = w’)<br /> Ở đây w là tất cả các biến trong inα,<br /> nhưng không thuộc V.<br /> 2.2. Chương trình như các thiết kế<br /> Để xác định ngữ nghĩa của chương trình,<br /> trước hết cần xác định một số toán tử trong các<br /> thiết kế. Cho hai thiết kế P1 và P2.<br />
Toán tử tuần tự: Nếu tập các ký tự ra của P1<br /> giống như tập các ký tự vào của P2, thành phần tuần<br /> tự của chúng được xác định như sau:<br /> 3<br /> <br /> T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br /> P1(input1,<br /> output2) def<br /> ∃m<br /> output2)<br /> <br /> •<br /> <br /> output1);<br /> <br /> định<br /> <br /> P1(input1,<br /> <br /> m)<br /> <br /> ∧<br /> <br /> P2(m,<br /> <br /> Trong đó: input1 và output1 là các<br /> tập ký tự vào và ra của P1. input2 và<br /> output2 là các tập ký tự vào và ra của P2.<br />
Toán<br /> <br /> tử<br /> <br /> c ::= | skip | chaos bỏ qua | không xác<br /> <br /> P2(input2,<br /> <br /> chọn<br /> <br /> có<br /> <br /> điều<br /> <br /> | var T x = e | end x<br /> khai báo<br /> <br /> | c; c | c
<br />
b<br /> c trình tự | chọn theo điều<br /> kiện<br /> <br /> kiện:<br /> <br /> ⊲P2) def (b ∧ P1) ∨ (¬<br /> ¬b ∧ P2), ở<br /> (P1⊳b⊲<br /> đây b là biểu thức logic có thể nhận giá trị<br /> true hoặc false.<br />
Các toán tử lựa chọn không tiền định<br /> và tiền định:<br /> P1 ⊓ P2 def P1 ∨ P2, P1 ⊔ P2 def<br /> P1 ∧ P2<br />
Vòng lặp while b do P được xác<br /> định như là điểm bất định nhỏ nhất: X =<br /> ((P; X)⊳<br /> ⊳b⊲<br /> ⊲ skip) của phương trình đệ qui<br /> X = F(X).<br /> 2.3. Biểu thức<br /> Một biểu thức có thể có một trong các<br /> dạng sau đây:<br /> <br /> 2.4. Các lệnh<br /> Phần này xem xét các lệnh và ngôn<br /> ngữ sẽ hỗ trợ các cấu trúc lập trình hướng<br /> đối tượng tiêu biểu. Một lệnh chung nhất có<br /> dạng:<br /> 4<br /> <br /> | c ⊓ c | b*c<br /> <br /> không tiền định | lặp<br /> <br /> | read(x: T)<br /> <br /> đọc giá trị kiểu T<br /> <br /> | le.m(e, v, u)<br /> <br /> gọi phương thức<br /> <br /> | le:=e | C.new(x) gán | tạo đối tượng mới.<br /> Ở đây b là biểu thức logic, c là lệnh, e là<br /> một biểu thức, le có thể xuất hiện ở vế trái của<br /> phép gán và có dạng le:= x | le.a với x là biến đơn<br /> còn a là thuộc tính của đối tượng. Chú ý rằng ở<br /> đây ký hiệu C (viết hoa) chỉ tên một lớp, còn c<br /> (viết thường) chỉ các lệnh.<br /> 2.5. Khai báo lớp<br /> Một chương trình hướng đối tượng có thể<br /> được chỉ ra bởi dạng cdecls•P. Nó bắt đầu bằng<br /> phần khai báo một số lớp, tiếp sau là khối lệnh P<br /> biểu diễn phương thức main của chương trình có<br /> dạng (glb, c). Phần khai báo lớp cdecls là một số<br /> hữu hạn các khai báo cdecl1; cdecl2; ...; cdeclk,<br /> mỗi cdecli có dạng như sau:<br /> <br /> e ::= x | null | new N | e is N | (N)e<br /> | e.a | f(e) | self<br /> Trong đó: x là một biến đơn, null<br /> biểu diễn đối tượng đặc biệt của lớp đặc<br /> biệt NULL là lớp con của mọi lớp và null<br /> là duy nhất; new N là tạo đối tượng mới<br /> của N; e is N là biểu thức kiểm thử (test);<br /> (N)e là biểu thức ép kiểu; e.a là biểu thức<br /> thuộc tính, f(e) là phép toán gắn liền với<br /> các kiểu nguyên thuỷ; self được sử dụng<br /> để chỉ đối tượng hoạt động trong phạm vi<br /> hiện tại.<br /> <br /> khai báo | kết thúc<br /> <br /> [private] class N [extends M] {<br /> pri: ; pro:; pub: ;<br /> meth:<br /> <br /> m1(x11: T11, y12: T12, z13: T13)<br /> <br /> {c1};<br /> ... ;<br /> mℓ(xℓ1 : Tℓ1, yℓ2: Tℓ2, zℓ3: Tℓ3) {cℓ}<br /> }<br /> Ở đây:<br />
N và M là tên các lớp và M được gọi là<br /> lớp cha của N.<br />
Phần pri khai báo các thuộc tính private<br /> a với các kiểu U và các giá trị khởi đầu u. Tương<br /> tự cho các phần pro và pub của lớp N.<br /> <br /> T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br />
Phần meth khai báo các phương<br /> thức, các tham biến giá trị xi: Ti1, các tham<br /> biến kết quả yi: Ti2, các tham biến giá trị-kết<br /> quả zi: Ti3 và các phần thân ci. Ta cũng sử<br /> dụng ký hiệu m(paras) { c } để chỉ sự khai<br /> báo các phương thức.<br /> <br /> Ở đây P đóng vai trò là phương thức chính<br /> (glb, c).<br /> <br /> 2.6. Tinh chế hệ thống đối tượng [3,<br /> <br /> trong đó, chương trình vế trái của ⊑ có<br /> một thành phần được làm mịn và vế bên phải có<br /> một chương trình kết quả của việc làm mịn.<br /> <br /> 11]<br /> Định nghĩa 1 (tinh chế thiết kế):<br /> Thiết kế D2 = (α, P2) là tinh chế của thiết<br /> kế D1=(α, P1) được chỉ ra bởi D1 ⊑ D2,<br /> nếu P2 dẫn tới P1, nghĩa là: ∀x, x’, ..., z, z’,<br /> ok, ok’ • (P2 ⇒ P1).<br /> Ở đây x, ..., z là các biến chứa trong<br /> α.. D1≡ D2 nếu và chỉ nếu D1⊑ D2 và D2<br /> <br /> ⊑ D1.<br /> Định nghĩa 2 (tinh chế dữ liệu): Cho<br /> ρ là ánh xạ (cũng có thể được coi như là<br /> thiết kế) từ α2 tới α1. Thiết kế D2 = (α2, P2)<br /> là tinh chế của thiết kế D1 = (α1, P1) dưới<br /> <br /> ρ, được chỉ ra bởi D1⊑ρ D2, nếu (ρ; P1)⊑<br /> (P2; ρ). Trong trường hợp này ρ được gọi<br /> là ánh xạ tinh chế.<br /> Định nghĩa 3 (tinh chế hệ thống):<br /> Cho S1 và S2 là các đối tượng chương trình<br /> có cùng một tập các biến chung glb. S1 là<br /> tinh chế của S2, được chỉ ra bởi S2 ⊑sys S1,<br /> nếu hành vi của nó có thể kiểm soát và dự<br /> đoán nhiều hơn trong S2, tức là: ∀ x, x’, ok,<br /> ok’ • (S1⇒ S2).<br /> Định nghĩa 4 (tinh chế lớp): Cho<br /> cdecls1 và cdecls2 là hai phần khai báo.<br /> cdecls1 tinh chế cdecls2, được chỉ ra bởi<br /> cdecls1 ⊒class cdecls2 nếu như phần trước có<br /> thể thay thế phần sau trong bất kỳ hệ thống<br /> đối tượng:<br /> cdecls1⊒class cdecls2 def<br /> <br /> ∀P • (cdecls1• P ⊒sys cdecls2•<br /> P).<br /> <br /> 2.7. Các luật làm mịn và chế tác lại<br /> Nói chung, một luật làm mịn và chế tác lại<br /> có dạng như sau: cdecls • P ⊑ cdecls1 • P1<br /> <br /> Khi viết các luật làm mịn, chúng ta sử<br /> dụng ký pháp sau để chỉ sự khai báo lớp N:<br /> N [M, pri, pro, pub, op]<br /> Trong đó, M là tên lớp cha của N; pri,<br /> pro và pub là các tập thuộc tính private,<br /> protected và public của N; op là tập các<br /> phương thức của N. Ta có thể chỉ đưa ra các<br /> tham số liên quan cần thiết chẳng hạn như,<br /> nếu sử dụng N[op] để chỉ lớp N với tập các<br /> phương thức op, N[pro, op] chỉ lớp N với<br /> các thuộc tính protected là pro và các<br /> phương thức là op... Chi tiết về vấn đề làm<br /> mịn hệ thống đối tượng, các luật làm mịn và<br /> chế tác lại có thể xem trong trong [3, 5, 6, 7,<br /> 8, 9].<br /> Dựa trên mô hình rCOS đã trình bày ở<br /> trên, trong phần 3 chúng tôi sẽ xây dựng một số<br /> đặc tả cho việc thiết kế các hệ thống hướng đối<br /> tượng.<br /> 3. Xây dựng một số đặc tả cho thiết kế<br /> hướng đối tượng<br /> 3.1. Đặc tả hệ thống<br /> Một hệ thống đối tượng S = (α, P), trong<br /> đó P có dạng p(x) ⊢ R(x, x’) và α gồm 3 thành<br /> phần như sau:<br /> 1) Phần thứ nhất: Cung cấp các thông tin<br /> ngữ cảnh lớp và các quan hệ của chúng:<br />
cname: Tập các tên lớp đã được khai<br /> báo.<br />
superclass: Là ánh xạ từ một tên lớp tới<br /> tên lớp cha của nó.<br /> 5<br /> <br /> T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br /> 2) Phần thứ hai: Mô tả chi tiết cấu<br /> trúc của mỗi lớp: với mỗi tên lớp N ∈<br /> cname, nó bao gồm:<br />
attribute(N): Là ánh xạ từ một lớp<br /> N tới tập các thuộc tính được khai báo của<br /> nó, tập thuộc tính có dạng . Trong<br /> đó a là tên thuộc tính, T là kiểu và d là giá<br /> trị khởi đầu.<br />
Attribute là hàm mở rộng của<br /> attribue(N), với mỗi lớp N bao gồm các<br /> thuộc tính protected và public mà N được<br /> kế thừa từ các lớp ông cha của nó.<br />
meth(N): Là ánh xạ từ một lớp N tới<br /> tập các phương thức được khai báo hoặc kế<br /> thừa của N, tập phương thức có dạng:<br /> m → (, D),<br /> hoặc:<br /> <br /> Trong đó N là tên lớp, a là tên thuộc tính,<br /> T là kiểu thuộc tính và d là trị khởi đầu.<br /> Ở đây ta chỉ quan tâm tới việc đưa ra một<br /> số thuật toán xử lý các lớp, tinh chế và làm mịn<br /> các thành phần dữ liệu, các quan hệ giữa chúng<br /> trong phần khai báo cdecls, nên thành phần P<br /> của hệ thống không thay đổi. Vấn đề cần phải<br /> giải quyết là đưa ra các cách đặc tả các lớp và<br /> các thuật toán xử lý trên các lớp của hệ thống<br /> được mô tả như vậy.<br /> Trong khuôn khổ bài báo này, chúng tôi sẽ<br /> trình bày phương pháp đặc tả mối lớp bằng một<br /> tệp văn bản (text), tương ứng với cách đặc tả lớp<br /> này là xây dựng các thuật toán làm mịn thông<br /> qua việc xử lý sự biến đổi nội dụng của tệp văn<br /> bản đó.<br /> 3.2. Đặc tả mỗi lớp bằng một tệp văn bản<br /> <br /> m → (paras, D)<br /> <br /> Trong đó: m là tên phương thức và<br /> có x, y và z tương ứng là tham biến giá trị,<br /> tham biến kết quả và tham biến giá trị-kết<br /> quả của nó; Tx, Ty và Tz là các kiểu dữ<br /> liệu. Thiết kế D biểu diễn hành vi của<br /> phương thức m.<br /> 3) Phần thứ ba: Nhận biết các biến<br /> mà chương trình sử dụng:<br /> <br /> 3.2.1. Mô tả hệ thống bằng các tệp văn<br /> bản<br /> Trong cách mô tả hệ thống này, chúng tôi<br /> sử dụng một tệp văn bản để đặc tả các thành<br /> phần của một lớp và biểu diễn quá trình biến đổi<br /> của nó trong hệ thống, nghĩa là thành phần α của<br /> hệ thống là một là một tập các file văn bản, mỗi<br /> file văn bản đặc trưng cho một lớp bao gồm các<br /> thành phần:<br /> <br />
alphabet: Tập các biến chung cùng<br /> với kiểu của chúng đã biết trong chương<br /> trình, nó có dạng . Ở đây, x là tên<br /> biến, T là kiểu của x.<br /> <br />
name: tên lớp<br /> <br />
locvar: Tập các biến địa phương có<br /> dạng . Trong đó v là tên biến, T là kiểu<br /> của nó.<br /> <br />
pro: các thuộc tính protected<br /> <br />
visibleattr: Tập các thuộc tính<br /> tường minh trong lớp hiện tại, tức là tất cả<br /> thuộc tính đã được khai báo thuộc miền<br /> private, protected và public (đã khai báo)<br /> của lớp. Nó bao gồm 3 ánh xạ:<br /> pri: N → , pro: N → ,<br /> pub: N → <br /> 6<br /> <br />
supername: tên lớp cha<br />
pri: các thuộc tính private<br />
pub: các thuộc tính public<br />
meth:các phương thức<br /> Trong file văn bản đặc tả lớp như trên:<br /> Thành phần mô tả tên lớp name bắt buộc<br /> phải có (khác trống) và không thay đổi; Các<br /> thành phần khác có thể có hoặc không và sẽ<br /> thay đổi trong quá trình hoạt động của hệ<br /> thống, do các xử lý như thêm bớt các thuộc<br /> tính hay phương thức, thay đổi tính visibility<br /> của lớp…<br /> <br /> T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008<br /> <br /> Để quản lý các lớp trong hệ thống, ta<br /> sẽ sử dụng một tệp văn bản cname.txt. Khi<br /> hệ thống bắt đầu khởi động thì tệp<br /> cname.txt mà nội dung của nó là trống lập<br /> tức được tạo ra. Hàm tạo ra tệp này có thể<br /> được viết bằng C++ như sau:<br /> // Tao file cname.txt de luu class //<br /> names<br /> class cnameFile {<br /> public:<br /> void cname() {<br /> ofstream outfile;<br /> outfile.open("cname.txt");<br /> outfile.close();<br /> }<br /> };<br /> Khi một lớp được tạo ra trong hệ thống<br /> thì tên của nó sẽ được bổ sung ngay vào trong<br /> tệp này.<br /> Để quản lý sự thay đổi của các lớp<br /> trong hệ thống chúng ta cần phải xây dựng<br /> các hàm sau cho mỗi lớp:<br />
pri(C) trả về xâu có dạng <br /> | U a = u, mô tả tập các thuộc tính private<br /> của lớp C. Nó được xác định từ thành phần<br /> pri của tệp C.txt.<br />
pro(C) trả về xâu có dạng <br /> | U b = v, mô tả tập các thuộc tính protected<br /> của lớp C. Nó được xác định từ thành phần<br /> pro của tệp C.txt.<br />
pub(C) trả về xâu có dạng | U c = w, mô tả tập các thuộc tính public<br /> của lớp C. Nó được xác định từ thành phần<br /> pub của tệp C.txt.<br />
attr(C) hàm trả về xâu là pri(C) ∪<br /> pro(C) ∪ pub(C).<br />
super(C) trả về tên lớp cha của lớp<br /> C nếu có, nếu lớp C không có cha thì trả về<br /> <br /> một xâu trống. Nó được xác định từ thành phần<br /> super của tệp C.txt.<br />
meth(C) trả về tập các phương thức của<br /> lớp C. Nó được xác định từ thành phần meth của<br /> tệp C.txt.<br />
alpha(cdecls) trả về tập các biến dùng<br /> chung.<br />
locvar(C) trả về xâu biểu diễn tập các<br /> biến cục bộ của lớp C, nó được xác định từ tệp<br /> thành phần meth của tệp C.txt.<br />
Attr là sự mở rộng của attr(C), với mỗi<br /> lớp C nó bao gồm các thuộc tính protected và<br /> public mà lớp C được kế thừa từ các lớp cha của<br /> nó.<br />
Meth(C) trả về tập các phương thức mà<br /> lớp C được kế thừa từ lớp cha.<br />
ATTR(cdecls) là tập { C.a | C ∈ cname<br /> ∧ a ∈ Attr(C) }<br /> Sau đây chúng tôi sẽ đưa ra một số đặc tả<br /> thuật toán làm mịn hình thức, dựa trên mô hình<br /> của hệ thống hướng đối tượng đã nêu ra, để thực<br /> hiện một số công việc tinh chế và làm mịn phần<br /> khai báo trong hệ thống, làm cơ sở cho việc phát<br /> triển mô hình thiết kế trên UML sau này.<br /> 3.2.2. Đặc tả các thuật toán làm mịn<br /> Các thuật toán làm mịn ở đây đều sử dụng<br /> luật 11 trong [3] và một hoặc một số luật khác<br /> trong [3, 5, 9]. Do đó trong các thuật toán sau, ta<br /> không nhắc lại việc sử dụng luật 11 mà chỉ đề<br /> cập tới các luật khác được sử dụng thêm.<br /> 3.2.2.1. Thuật toán thêm một tên lớp vào<br /> hệ thống<br /> Thêm một tên lớp mới C vào phần khai<br /> báo của một hệ thống, thì hệ thống sẽ được tinh<br /> chế theo luật làm mịn trong như sau: cdecls ⊑<br /> C; cdecls.<br /> Thêm một lớp trống C (lớp chỉ có tên và<br /> chưa có một thuộc tính hay phương thức nào)<br /> vào trong một hệ thống S sẽ làm α thay đổi, cụ<br /> thể là thành phần cname của hệ thống sẽ thay<br /> 7<br /> <br />