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

Nội dung bài viết là trình bày tóm tắt mô hình tính toán rCOS đã được He Jifeng và cộng sự đề xuất và phát triển [3]. Phần 3 là đề xuất mới về việc áp dụng rCOS vào việc xây dựng một số đặc tả hệ thống phục vụ cho phát triển hệ thống phần mềm theo phương pháp hướng đối tượng.
Nội dung trích xuất từ tài liệu:
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 MỘT CÁCH ĐẶC TẢ THIẾT KẾ 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) 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 nền tảng cho việc phát triển phần mềm hướng đối tượng. Bài báo này sẽ giới thiệu lý thuyết lập trình thống nhất của Hoare và He [2] 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. Lý thuyết lập trình được vận dụng để trình bày ngữ nghĩa của ngôn ngữ lập trình hướng đối tượng với các lớp, tính rõ ràng, liên kết động, các phương thức đệ quy và tính đệ quy. Để cho đơn giản, những gì liên quan đến các định nghĩa hình thức về biến, tham chiếu tới các kiểu được bỏ qua (có thể xem trong [2, 5]). Phần 2 của bài báo là trình bày tóm tắt mô hình tính toán rCOS đã được He Jifeng và cộng sự đề xuất và phát triển [3]. Phần 3 là đề xuất mới về việc áp dụng rCOS vào việc xây dựng một số đặc tả hệ thống phục vụ cho phát triển hệ thống phần mềm theo phương pháp hướng đối tượng. 2. Mô hình tính toán rCOS [3] Một chương trình lệnh được xác định bằng quan hệ nhị phân (α, P) [2, 5, 11], trong đó: α ký hiệu tập các biến đã biết trong chương trình. P là tân từ quan hệ các giá trị của các biến trong chương trình khi khởi tạo với các giá trị cuối của chúng, P còn được gọi là thiết kế (design). Với chương trình tuần tự lệnh, ta quan tâm theo dõi các giá trị của các biến vào inα và các biến ra outα. Ở đây ta đưa ra qui ước rằng với mỗi biến x ∈ inα, phiên bản x’ của nó là một biến ra trong outα, mang giá trị cuối của x sau khi thực hiện chương trình. Ta dùng biến logic ok chỉ ra một chương trình có khởi tạo đúng hay không và phiên bản ok’ của nó biểu diễn sự thực hiện có kết thúc hay không. Bảng ký tự α được định nghĩa là inα ∪ outα ∪ {ok, ok’} và thiết kế có dạng: p(x) ├ R(x, x’) def ok ∧ p(x) ⇒ ok’ ∧ R(x, x’) Trong đó: p là tân từ trên inα và R là tân từ trên outα; p là tiền điều kiện, xác định trạng thái khởi đầu của chương trình; R là hậu điều kiện, xác định trạng thái kết thúc của chương trình; 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’ tương ứng mô tả trạng thái 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. 2.1. Thiết kế Một thiết kế biểu diễn sự thoả thuận giữa “người sử dụng” và chương trình, nếu chương trình được khởi tạo một cách hợp thức trong trạng thái thoả mãn tiền điều kiện p thì nó sẽ kết thúc trong trạng thái thoả mãn hậu điều kiện R. Một thiết kế V thường có dạng sau: V: (p├ R) def p ⊢ (R ∧ w = w’) Ở đây w là tất cả các biến trong inα, nhưng không thuộc V. 2.2. Chương trình như các thiết kế Để xác định ngữ nghĩa của chương trình, trước hết cần xác định một số toán tử trong các thiết kế. Cho hai thiết kế P1 và P2.
Toán tử tuần tự: Nếu tập các ký tự ra của P1 giống như tập các ký tự vào của P2, thành phần tuần tự của chúng được xác định như sau: 3 T¹p chÝ Khoa häc & C«ng nghÖ - Sè 1(45) Tập 2/N¨m 2008 P1(input1, output2) def ∃m output2) • output1); định P1(input1, m) ∧ P2(m, Trong đó: input1 và output1 là các tập ký tự vào và ra của P1. input2 và output2 là các tập ký tự vào và ra của P2.
Toán tử c ::= | skip | chaos bỏ qua | không xác P2(input2, chọn có điều | var T x = e | end x khai báo | c; c | c

b c trình tự | chọn theo điều kiện kiện: ⊲P2) def (b ∧ P1) ∨ (¬ ¬b ∧ P2), ở (P1⊳b⊲ đây b là biểu thức logic có thể nhận giá trị true hoặc false.
Các toán tử lựa chọn không tiền định và tiền định: P1 ⊓ P2 def P1 ∨ P2, P1 ⊔ P2 def P1 ∧ P2
Vòng lặp while b do P được xác định như là điểm bất định nhỏ nhất: X = ((P; X)⊳ ⊳b⊲ ⊲ skip) của phương trình đệ qui X = F(X). 2.3. Biểu thức Một biểu thức có thể có một trong các dạng sau đây: 2.4. Các lệnh Phần này xem xét các lệnh và ngôn ngữ sẽ hỗ trợ các cấu trúc lập trình hướng đối tượng tiêu biểu. Một lệnh chung nhất có dạng: 4 | c ⊓ c | b*c không tiền định | lặp | read(x: T) đọc giá trị kiểu T | le.m(e, v, u) gọi phương thức | le:=e | C.new(x) 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. Chú ý rằng ở đây ký hiệu C (viết hoa) chỉ tên một lớp, còn c (viết thường) chỉ các lệnh. 2.5. Khai báo lớp Một chương trình hướng đối tượng có thể được chỉ ra bởi dạng cdecls•P. Nó bắt đầu bằng phần khai báo một số lớp, tiếp sau là khối lệnh P biểu diễn phương thức main của chương trình có dạng (glb, c). Phần khai báo lớp cdecls là một số hữu hạn các khai báo cdecl1; cde ...