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. | 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α ∪
