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

3

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: