Chương 1 KIẾN THỨC CƠ SỞ Trong chương này, các Mục 1.2 sẽ lần lượt trình bày về ngôn ngữ ràng buộc đối tượng (OCL) và lôgic vị từ bậc một (FOL), đây là các phương tiện sử dụng để biểu diễn hành vi cần kiểm chứng của mô hình phần mềm.3 mô tả một cách tóm tắt bài toán kiểm chứng tính nhất quán đã được thực hiện trong các nghiên cứu trước đây. Việc giới thiệu lại bài toán này nhằm mục tiêu giúp người đọc có được cái nhìn rõ hơn về kiến trúc được đề xuất của công cụ CVT.1 Ngôn ngữ ràng buộc đối tượng OCL Ngôn ngữ ràng buộc đối tượng OCL (Object Constraint Language) ra đời nhằm mục tiêu khắc phục các hạn chế của UML trong việc biểu diễn một cách chính xác các khía cạnh chi tiết của bản thiết kế hệ thống [13]. OCL được phát triển lần đầu bởi tổ chức IBM vào năm 1995 và được tích hợp vào UML năm 1997. Thời gian đầu, OCL chỉ được sử dụng như là một ngôn ngữ ràng buộc đối tượng bổ sung cho UML, tuy nhiên nó nhanh chóng được mở rộng phạm vi và trở thành một thành phần quan trọng trong bất kỳ kỹ nghệ hướng mô hình nào.
OCL được coi như một ngôn ngữ mặc định dùng biểu diễn các truy vấn trên mô hình hoặc siêu mô hình, thực hiện và đặc tả các yêu cầu. OCL cũng thường được sử dụng để mô tả các phép biến đổi mô hình (như là một phần của các mô hình nguồn và mô hình đích trong các quy tắc biến đổi), biểu diễn sự hợp lệ của các quy tắc (như là một phần của định nghĩa đặc tả các miền mới), hoặc các mẫu sản sinh mã nguồn (mô tả các mẫu và quy tắc sản sinh mã), v. Để đáp ứng các mục tiêu này, OCL được phát triển và phát hành một số các phiên bản. OCL được 7 Đề tài nghiên cứu khoa học cấp trường năm học 2017-2018 8 phát triển như là một chuẩn công nghiệp bởi tổ chức Object Management Group 1 (OMG) [14].
Phiên bản mới nhất của OCL là 2.4 được ra đời vào năm 2014, phiên bản này tương thích với phiên bản 2. Mỗi biểu thức trong OCL đều xác định một kiểu nhất định (kiểu này có thể được định nghĩa trước trong OCL hoặc là một kiểu được định nghĩa trong mô hình với các ràng buộc được mô tả bởi OCL). Kiểu của các biểu thức trong OCL cũng phải phù hợp với các quy tắc và các phép toán được áp dụng trên kiểu đó. Chú ý rằng OCL chỉ là một ngôn ngữ đặc tả thuần túy, bởi vậy khi các biểu thức OCL được thực thi, nó không gây bất cứ ảnh hưởng nào đến trạng thái của mô hình phần mềm mà nó đặc tả.
Ngoài ra, tất cả các vấn đề liên quan đến cài đặt cũng nằm ngoại phạm vi và không thể biểu diễn bằng OCL. OCL có thể được sử dụng để mô tả nhiều loại ràng buộc khác nhau trong mô hình UML, sau đây là một số loại ràng buộc tập trung chủ yếu vào tác dụng của nó trên biểu đồ lớp: – Biểu diễn các ràng buộc bất biến của lớp (class invariants); – Khởi tạo giá trị cho thuộc tính của các biến trong biểu thức OCL; – Biểu diễn cách tính giá trị của các phần tử dẫn xuất dựa trên giá trị của các phần tử nguồn; – Thực hiện các câu lệnh truy vấn; – Biểu diễn tiền/hậu điều kiện (pre/post-conditions) của các phương thức có trong mô hình. Các khả năng biểu diễn trên của OCL sẽ lần lượt được cụ thể hóa như sau: OCL được dùng để biểu diễn các ràng buộc bất biến (Invariants): Các ràng buộc toàn vẹn trong OCL được biểu diễn dưới dạng các bất biến được định nghĩa trong một Context cụ thể, với tên của Context là kiểu của ràng buộc. Phần thân của context, là các điều kiện logic (sau từ khóa inv) phải được kiểm tra và thỏa mãn bởi tất cả các thể hiện của Context đó.
Các bất biến là các biểu thức được sử dụng phổ biến nhất trong OCL vì nó cho phép các nhà thiết kế dễ dàng đặc tả tất cả các loại điều kiện mà hệ thống phải tuân thủ. Ngoài ra, bất biến còn có thể hạn chế giá trị của các đối tượng đơn lẻ. Biểu thức dưới đây phát biểu rằng, tất cả các quotes phải có giá trị dương. Chú ý rằng biến self đại diện cho một thể hiện tùy ý của lớp Quote và dấu chấm được sử dụng để truy cập vào các tính chất (thuộc tính hoặc phương thức) của 1.org/ Đề tài nghiên cứu khoa học cấp trường năm học 2017-2018 9 biến self trong lớp Quote.
Tất cả các thể hiện của lớp Quote phải được đánh giá là thỏa mãn bất biến này và biến (self) đương nhiên cũng phải thỏa mãn ràng buộc bất biến đó. 1 context Quote inv QuoteOverZero: self.value > 0 OCL sử dụng để khởi tạo giá trị cho thuộc tính của các biến: OCL có thể được sử dụng để khởi tạo giá trị ban đầu cho các thuộc tính của một đối tượng khi đối tượng đó được tạo ra. Để thực hiện công việc này, kiểu của biểu thức OCL khởi tạo và kiểu của thuộc tính được dùng khởi tạo phải phù hợp với nhau. Biểu thức OCL sau đây khởi tạo giá trị là false cho thuộc tính premium của Customer (trạng thái của premium sẽ được chuyển thành true khi khách hàng đã thuê một số xe).
1 context Customer::premium: boolean init: false Biểu thức OCL xác định các quy tắc tính toán giá trị của các thuộc tính trong mô hình dẫn xuất: các phần tử dẫn xuất là các phần tử mà có giá trị được suy dẫn từ các giá trị của các phần tử thuộc vào mô hình nguồn. OCL là một lựa chọn phổ biến cho việc xác định các quy tắc dẫn xuất này. Hãy xem xét quy tắc sau đây cho việc chiết khấu các phần tử dẫn xuất từ lớp Customer, phát biểu rằng các khách hàngs có trạng thái của thuộc tính premium là true thì được hưởng 30%, các khách hàng có trạng thái của thuộc tính premium là false và có ít nhất 5 chiếc xe cho thuê thì được giảm giá 15%, còn lại tất cả các khách hàng khác đều không được giảm giá. 1 context Customer::discount: integer derive: 2 if not self.premium then 3 if self.category=’high’)->size()>=5 4 then 15 else 0 endif 5 else 30 endif Quy tắc này trong OCL sẽ cho phép tính các giá trị dẫn xuất phù hợp với từng trường hợp tương ứng.
Câu lệnh truy vấn: biểu thức OCL dạng này thực hiện truy vấn trên cơ sở dữ liệu hệ thống và trả về thông tin cho người dùng. Câu lệnh truy vấn sau sẽ trả về giá trị là true nếu chiếc car là chiếc được dùng nhiều nhất trong hệ thống xe cho thuê. 1 context Car::mostPopular(): boolean Đề tài nghiên cứu khoa học cấp trường năm học 2017-2018 10 2 body: Car::allInstances()->forAll(c1|c1<>self 3 implies c1.rentalAgreement->size()<=self.rentalAgreement->size()) Biểu diễn tiền/hậu điều kiện của các phép toán: có hai cách tiếp cận để kiểm tra sự thỏa mãn của các ràng buộc về tiền/hậu điều kiện đối với các phép toán. Cách thứ nhất là dùng các câu lệnh chỉ thị và cách thứ hai là đặc tả các ràng buộc thông qua hợp đồng (contract).
Trong cách tiếp cận đầu tiên, người thiết kế xác định rõ ràng tập các câu lệnh cấu trúc và các cấu trúc này sẽ được thực thi khi thực hiện phép toán. Theo cách tiếp cận thứ hai, nhà thiết kế sẽ cung cấp cho mỗi hoạt động một hợp đồng của nó. Mỗi hợp đồng bao gồm một tập các điều khoản về tiền/hậu điều kiện. Tiền điều kiện xác định một tập hợp các ràng buộc đầu vào trước khi hoạt động được thực thi, còn hậu điều kiện cho biết các ràng buộc mà hệ thống phải thỏa mãn khi kết thúc giao dịch.
OCL là ngôn ngữ thường được lựa chọn để biểu diễn cho tiền/hậu điều kiện của hoạt động mức độ mô hình. 1 context Rental::newRental(id:Integer, price:Real, startingDate:Date, 2 endingDate:Date, customer:Customer, carRegNum:String, pickupBranch: Branch, dropOffBranch: Branch) 3 pre: customer.licenseExpDate>endingDate 4 post: Rental.endingDate=endingDate and r.startingDate= startingDate 6 and r.driver=customer and r.pickupBranch=pickupBranch and r. dropOffBranch=dropOffBranch 7 and r.regNum=carRegNum)) Biểu thức tiền điều kiện được đặt sau từ khóa pre và hậu điều kiện được đặt sau từ khóa post. Trong phần này, đề tài đã mô tả một số đặc trưng cơ bản của ngôn ngữ ràng buộc đối tượng OCL.
Các biểu thức về bất biến, tiền/hậu điều kiện sẽ là các đối tượng nghiên cứu chính của đề tài.2 Lôgic vị từ bậc 1 Lôgic vị từ bậc 1 (FOL) [9] cung cấp cho chúng ta khả năng biểu diễn các biểu thức logic mệnh đề (propositional logic) và cách thức định lượng hóa trên các đối tượng. Nhờ vào các lượng từ trong FOL chúng ta có thể mô tả các đối tượng và mối quan hệ giữa chúng một cách chính xác. Đây chính là ưu điểm của FOL so Đề tài nghiên cứu khoa học cấp trường năm học 2017-2018 11 với logic mệnh đề. FOL có thể dùng để biểu diễn lý thuyết số, lý thuyết tập hợp và thậm chí biểu diễn sự tính toán trong máy Turing.
Sau đây là một số ký hiệu cơ bản được sử dụng để xây dựng các công thức FOL. Các ký hiệu này được trình bày đầy đủ trong [9]. Các phép toán kết hợp (Logical connectives) (⇒, ∧, ∨, và ⇔), phủ định (¬), và dấu ngoặc. Các phép toán này được sử dụng một để tạo nên các công thức FOL phức hợp.
Các ký hiệu hằng (Constants symbols) là các chuỗi (a, b, c, v.) dùng để biểu diễn thay thế cho các đối tượng. Các ký hiệu biến (Variable symbols) sẽ được sử dụng như những “place holders” cho việc định lượng hóa trên các đối tượng. Các ký hiệu vị từ (Predicate symbols) mỗi ký hiệu được liên kết với arity (ví dụ, số lượng các đối số), có thể là 0 hoặc một số xác định khác. Vị từ được dùng để biểu diễn cho thuộc tính của các đối tượng và mối quan hệ giữa chúng.
Các ký hiệu hàm (Function symbols) mỗi ký hiệu được đặc tả bởi arity (ví dụ, số lượng các đối số nhập vào) đây là một hàm ánh xạ từ một số lượng các đối tượng đến các đối tượng. Các lượng từ với mọi và tồn tại (Universal and existential quantifier symbols) dùng để định lượng hóa trên các đối tượng.3 Tổng quan về bài toán kiểm chứng tính nhất quán trong tái cấu trúc hệ thống phần mềm Trong một nghiên cứu trước đây [15], chúng tôi đã đề xuất phương pháp kiểm chứng tính nhất quán của hệ thống phần mềm trước và sau khi tái cấu trúc. Phương pháp kiểm chứng được mô tả như trong Hình 1.1 bao gồm các tiến trình sau: (1) Tái cấu trúc mô hình phần mềm (Refactoring), (2) Tính toán tiền/hậu điều kiện của các kịch bản trước và sau tái cấu trúc, và (3) kiểm tra tính nhất quán.