Luận văn Chuyển đổi đặc tả UML với OCL sang đặc tả ALLOY

ên là Company inv : seft. numberOfEmployees > 50 --Khai báo một bất biến. Ý nghĩa : Mọi thể hiện của đối tượng Company phải thỏa mãn ràng buộc numberOfEmployees > 50 tại mọi thời điểm. Từ khóa seft tham chiếu tới thể hiện của đối tượng Company, sử dụng toán tử “.” để chỉ tới thuộc tính numberOfEmployees của đối tượng Company. 1.2.2.3 Tiền điều kiện và hậu điều kiện – pre & post condition Tiền điều kiện và hậu điều kiện là các ràng buộc liên kết tới phương thức của một phân loại lớp. Mục đích của tiền điều kiện là chỉ rõ điều kiện phải có trước khi phương thức thực thi. Tiền điều kiện chứa một biểu thức OCL[5] (trả về kết quả Boolean). Biểu thức OCL[5] này phải được đánh giá là đúng bất cứ khi nào phương thức bắt đầu thực thi, nhưng việc đánh giá này chỉ áp dụng cho thể hiện thực thi phương thức.Mục đích của hậu điều kiện là chỉ rõ điều kiện phải có sau khi thực thi phương thức. Hậu điều kiện cũng được biểu diễn bằng một biểu thức OCL[5] (trả về kết quả Boolean). Việc đánh giá biểu 8 thức OCL[5] tại thời điểm kết thúc thực thi phương thức. Bên trong ràng buộc tiền điều kiện không sử dụng toán tử @pre nhưng bên trong ràng buộc hậu điều kiện có thể sử dụng @pre để tham chiếu tới giá trị của tiền điều kiện[5]. Cú pháp[5]: context Typename::operationName(para1 : Type1, para2 : Type2,...)Return Type pre: --Khai báo các tiền điều kiện post: --Khai báo các hậu điều kiện hoặc: context Typename::operationName(para1 : Type1, para2 : Type2,...)Return Type pre preconditionName : --Khai báo tiền điều kiện post postconditionName: --Khai báo hậu điều kiện Ví dụ : context Person::income(d : Date) Return interger pre preOK: d > 0 --Tiền điều kiện: đảm bảo d > 0 post postOK: result > 5000 --Hậu điều kiện đảm bảo trả về kết quả > 5000. 1.2.2.4 Ngữ cảnh gói – package context Một biểu đồ UML[1] thường có nhiều biểu đồ con trong đó. Do vậy OCL[5] cung cấp cho chúng ta cặp từ khóa package và endpackage để làm tăng sự rõ ràng khi nhóm lại các khai báo các bất biến, tiền điều kiện hậu điều kiện... thuộc về cùng một ngữ cảnh nào đó trong cụm từ khóa package và endpackage. Cú pháp[5]: package Package::SubPackage --Bắt đầu bằng từ khóa package context X inv : --Khai báo các bất biến context X ::operationName(para1 : Type1, para2: Type2,...) Return Type pre preconditionName : --Khai báo các tiền điều kiện post postconditionName: --Khai báo các hậu điều kiện ... endpackage --Kết thúc với từ khóa endpackage 1.2.2.5 Biểu thức bodyB Biểu thức body là một biểu thức kiên kết tới một phương thức của phân loại lớp. Nó được đánh dấu tới một phương thức truy vấn. Hành vi của một biểu thức OCL[5] như 9 một body phương thức phải thỏa mãn kiểu kết quả trả về của phương thức. Biểu thức body có thể sử dụng lẫn với các biểu thức trong ràng buộc tiền điều kiện và hậu điều kiện. Cú pháp[5]: context TypeName::operation(para1 : Type1, para2 : Type2...): Return Type body : --Biểu thức OCL. Ví dụ [5]: context Person::getCurrentSpouse(): Person pre : seft.isMarried = true body : seft.mariages->select(m | m.ended = false).spouse 1.2.2.6 Giá trị khởi tạo và giá trị dẫn xuất – Initial and Derived Values Một biểu thức khởi tạo giá trị là một biểu thức được liên kết tới một thuộc tính của một phân loại lớp hoặc một mút liên kết – association End. Giá trị khởi tạo thuộc tính bởi biểu thức phải phù hợp với kiểu của thuộc tính được đinh nghĩa trước đó trong phân loại lớp. Tương tự, giá trị khởi tạo của một liên kết phải phù hợp với loại mút liên kết. Ví dụ như, giá trị khởi tạo của mút liên kết là loại đính kèm với phân loại lớp khi số liên kết tối đa là một, khi mút liên kết nhiều hơn một thì phải là một OrderedSet. Một biểu thức dẫn xuất cũng là một biểu thức được liên kết tới một thuộc tính của một phân loại lớp hoặc là một liên kết cuối. Giá trị thuộc tính dẫn xuất tạo ra bởi biểu thức OCL[5] cũng phải phù hợp với kiểu của thuộc tính được định nghĩa trước đó. Khác với biểu thức khởi tạo giá tri, biểu thức dẫn xuất là một bất biến. Giá trị thuộc tính, hoặc giá trị liên kết cuối luôn bằng giá trị được đánh giá trong biểu thức dẫn xuất[5]. Cú pháp[5] : Khởi tạo giá trị thuộc tính : context TypeName::AtributeName:Type init : --Biểu thức OCL để khởi tạo giá trị thuộc tính Dẫn xuất giá trị mút liên kết[5] context TypeName::associcationRoleName:Type derived: --Biểu thức OCL để dẫn xuất giá trị liên kết Ví dụ[5]: context Person::income:Interger --Khởi tạo giá trị thuộc tính income của đối tượng Person init: parents.income->sum()*1% derived: if underAge then parents.income->sum()*1% 10 else job.salary endif 1.2.2.7 Biểu thức let Một biến hoặc chức năng được định nghĩa bởi biểu thức let có thể được sử dụng đồng nhất giống như thuộc tính, phương thức của một lớp. Và biểu thức let chỉ được sử dụng trong một biểu thức OCL[5], điều này gần giống như việc khai báo biến, phương thức của một lớp là kiểu private .Các biến trong biểu thức let phải được định kiểu và khởi tạo giá trị trước khi sử dụng trong biểu thức OCL[5]. Ví dụ: context Person inv : let income : Interger = self.job.salary->sum() in --Khai báo biểu thức let, income được khai báo kiểu interger và được khởi tạo giá trị if isUnemployed then income < 100 else income > 100 endif 1.2.2.8 Biểu thức def Một ràng buộc được định nghĩa trong biểu thức def được liên kết tới một lớp. Trong biểu thức def có thể chứa các biểu thức let. Việc khai báo biểu thức là def cũng tương ứng như việc khai báo một biến, phương thức có dạng public trong lập trình hướng đối tượng. Và khi đó biểu thức dạng def được sử dụng bởi các biểu thức OCL[5] khác nhau. Ví dụ[5]: context Person --Khai báo ngữ cảnh mà sẽ khai báo các biểu thức def def : income:Interger = seft.job.salary->sum() def: hasTitle(t: String):Boolean = seft.job->exists(title = t) --Sau khi khai báo biểu thức def như trên, thì biến income sẽ được sử dụng trong các biểu thức thuộc ngữ cảnh Person mà không cần khai báo lại. 1.2.3 Kiểu tập hợp và các phép toán trên tập hợp OCL cung cấp 4 kiểu tập hợp : Set, OrderedSet, Bag và Sequence và một tập hợp trừu tượng cho tất cả các kiểu tập hợp khác Collection 11 Bảng 1. Kiểu dữ liệu tập hợp trong OCL Kiểu tập hợp Ý nghĩa Set Tập bao gồm các phần tử toán học. Các phần tử trong tập hợp không được lặp lại. OrderedSet Là một Set. Nhưng các phần tử được sắp xếp theo thứ tự. Bag Là một tập hợp các phần tử cho phép sự lặp lại các phần tử. Sequence Tập bao gồm các phần tử được sắp xếp, và cho phép một phần tử được xuất hiện nhiều lần. Các phép toán trên Collection Bảng 2. Phép toán trên tập hợp OCL Phép toán Giá trị trả về Ý nghĩa =(c: Collection(T)) Boolean Trả về true nếu 2 tập hợp cùng kiểu và cùng có số lượng phần tử, thứ tự phần tử. (c:Collection(T)) Boolean Trả về true nếu 2 tập hợp không bằng nhau c->size() Interger Số lượng phần tử có trong tập hợp c->includes(object : T) Boolean true nếu object là một phần tử của tập hợp c->excludes(object : T) boolean Trả về giá trị true nếu object không thuộc tập hợp c c->count(object : T) interger Trả về số lần xuất hiện của phần tử object trong tập hợp c c1->includesAll(c2: Collection(T)) boolean Trả về true nếu c1 chứa tất cả phần tử c2 c->isEmpty() boolean Trả về true nếu c là tập rỗng hay số lượng phần tử là 0 c->notEmpty() boolean Trả về true nếu số phần tử của c lớn hơn 0 c->max() Type Trả về giá trị lớn nhất của tập hợp c, với kiểu 12 là Type (kiểu dữ liệu trong tập hợp c). Chỉ dùng cho tập có kiểu Interger và Real c->min() Type Trả về giá trị nhỏ nhất trong tập c. Chỉ dùng cho tập có kiểu Interger hoặc Real. c->sum() Type Trả về tổng các phần tử trong tập c. Áp dụng cho tập Interger và Real. c1->product(c2: Collection(T2)) Set(Tuple(first : T1, second : T2)) Phép tích đề các giữa 2 tập hợp trả về là 1 tập hợp. c->asSet() Set(T) Loại bỏ các phần tử lặp lại trong tập hợp c->asOrderedSet() OrderedSet(T) Trả về tập hợp OrderedSet c->asSequence() Sequence(T) Trả về tập hợp Sequence c->asBag() Bag(T) Trả về tập hợp Bag c->flatten() Collection(T2) Loại bỏ các phần tử không có cùng kiểu với kiểu dữ liệu của tập hợp 1.2.4 Biểu thức lặp trên tập hợp Các biểu thức lặp trên Colltection cũng đúng trên Set, OrderedSet, Bag và Sequence Bảng 3. Biểu thức lặp trên tập hợp OCL Collection Set OrderedSet Bag Sequence exists select select(ex: Oclexpression):OrderedSet(T) select select(expression :Oclexpression):Sequence(T) forAll reject reject(ex: Oclexpression):OrderedSet(T) reject reject isUnique collectNested collectNested(ex: Oclexpression):Sequence(T) collectNested collectNested any sortedBy sortedBy(ex: Oclexpression):OrderedSet(T) sortedBy sortedBy 13 one collect 1.3 Kết luận Như vậy trong chương 1, em đã trình bày những khái niệm cơ bản trong UML[1] và OCL[5]. Trọng tâm của chương một là trình bày về biểu đồ lớp, các thành phần của một lớp, liên kết giữa các lớp trong biểu đồ. Một điều dễ nhận thấy là UML[1] với hệ thống ký pháp trực quan giúp chúng ta dễ hiểu về hệ thống. Chúng ta sử dụng thêm OCL[5] để đặc tả các ràng buộc chặt chẽ hơn cho các yếu tố mô hình UML[1]. Tuy nhiên các công cụ đặc tả UML[1] với OCL[5] hiện nay không cung cấp khả năng tự đánh giá tính đúng đắn của mô hình được xây dựng ví dụ như việc kiểm tra tính đúng đắn của các ràng buộc OCL[5], hay khả năng tự sinh thể hiện cụ thể cho mô hình. Một giải pháp là chuyển đổi mô hình UML[1] sang mô hình Alloy[2] để có thể kiểm tra và sinh thể hiện từ đặc tả mô hình tự động bằng công cụ Alloy Analyzer[6]. Chương 2, em sẽ trình bày khái quát về Alloy[2], công cụ Alloy Analyzer[6]. Chương 2 . Giới thiệu Alloy và công cụ Alloy Analyzer 14 2.1 Khái quát về Alloy Lịch sử hình thành, phát triển: Alloy[2] được đưa ra và phát triển tại học viện công nghệ Massachusetts - Massachussets Instutite Techology của Mỹ. Người có công đóng góp lớn trong đó là giáo sư Daniel Jackson[6]. Alloy[2] là ngôn ngữ mô hình dựa trên logic vị từ bậc nhất. Mô hình Alloy[2] chứa các khai báo: ký hiêu- ký hiệu, sự kiện - fact,trường - field,mệnh đề- predicate, chức năng - function. Mỗi ký hiệu biểu diễn tập các nguyên tử - atoms thành phần thực thể cơ bản của Alloy[2]. Mỗi trường – field thuộc về một ký hiệu biểu diễn quan hệ giữa hai hoặc nhiều ký hiệu khác. Quan hệ trong Alloy[2] cũng giống như quan hệ trong cơ sở dữ liệu là tập các bộ nguyên tử. Có rất nhiều sự tương đồng giữa Alloy[2], biểu đồ lớp UML[1] và OCL[5]. Cụ thể như : Alloy[2] là ngôn ngữ mô hình hóa hướng đối tượng, Alloy[2] cũng có các quan hệ đặc trưng của hướng đối tượng như quan hệ kế thừa,...thêm nữa các khai báo bắt đầu với từ khóa sự kiện trong Alloy[2] là các ràng buộc vĩnh viễn, tức là bất cứ khi nào thực hiện mô hình thì thể hiện của mô hình phải thỏa mãn các ràng buộc trong sự kiện, điều này rất giống với các khai báo bất biến trong đặc tả OCL[5] đối với biểu đồ lớp, ngoài ra Alloy[2] là ngôn ngữ dựa trên logic vị từ bậc nhất do vậy nó dễ dàng biểu diễn các biểu thức ràng buộc logic, điều này giúp cho việc chuyển các đặc tả OCL[5] sang Alloy[2] được dễ dàng hơn. Alloy[2] chủ yếu được sử dụng để mô hình và phân tích các hệ thống phức tạp về mặt cấu trúc, hành vi ví dụ như các hệ thống: “name servers, network configuration protocols, acess control, telephony, scheduling, document structuring, key management, cryptography, instant messaging, railway switching, filesystem synchonization, sematic web”[6].Trong kỹ nghệ phần mềm Alloy[2] được “sử dụng chủ yếu ở giai đoạn đặc tả và phân tích và thiết kế hệ thống”[6]. 2.2 Mô hình Alloy Trong phần này chúng ta cùng tìm hiểu những khái niệm cơ bản về các phần cấu thành lên mô hình Alloy[2] và cách xây dựng một mô hình Alloy[2]. Một mô hình Alloy[2] thường chứa các khai báo bắt đầu với các từ khóa : sig, pred, func, check, run, fact. Các khai báo bắt đầu với từ khóa sig giống như khai báo bắt đầu với từ khóa class trong C++, theo sau khai báo bắt đầu với từ khóa pred là các mệnh đề logic, cũng tương tự như vậy với các từ khóa func, fact. Cụ thể: 2.2.1 Khai báo ký hiệu - signature Một ký hiệu giới thiệu một tập các nguyên tử. Một khai báo ký hiệu bắt đầu với từ khóa sig: sig A {} 15 giới thiệu một tập tên A. Thực sự thì một ký hiệu thì khác một tập hợp ở điểm, trong một ký hiệu chúng ta có thể khai báo thêm các quan hệ bên trong đó và có thể định nghĩa một kiểu mới. Một ký hiệu có thể là một mở rộng của một ký hiệu khác. Ví như : sig A extend B {}, thì A là một mở rộng của B. Một khai báo m sig A {} có ý nghĩa là số lượng A là m. Đây là một ràng buộc cho A. Một khai báo quan hệ bên trong một ký hiệu sẽ giống như khai báo một trường của ký hiệu đó. Một khai báo sig A { f: e } giới thiệu một quan hệ f trong miền A và khoảng biến thiên bị ràng buộc bởi biểu thức e. Xét về mặt ý nghĩa thì chúng ta có thể viết như sau : f: A -> e hoặc all this : A | this.f : e có nghĩa là nếu chúng ta có một thành phần đặc biệt là this luôn trỏ tới A thì tập hợp biểu diễn bởi this.f là một tập con của e. Bằng cách thêm vào lượng từ cho biểu thức e chúng ta có một khai báo dạng sig A {f : m e} khi đó this.f luôn luôn có m thành phần trong tập e. Alloy[2] cho phép chúng ta xây dựng các lớp trừu tượng bằng cách thêm từ khóa abstract trước khai báo một ký hiệu. Có thể khai báo các ký hiệu thừa kế từ lớp trừu tượng này. 2.2.2 Khai báo sự kiện - fact Một nhóm các ràng buộc có liên hệ và luôn luôn tồn tại và được thực thi cùng chương trình được tập hợp lại trong một sự kiện. Trong một mô hình Alloy[2] có thể tồn tại nhiều sự kiện khác nhau. Thứ tự các ràng buộc trong một sự kiện và thứ tự giữa các sự kiện trong mô hình Alloy[2] là không quan trọng, chúng được thực thi cùng lúc trong chương trình. Khai báo một sự kiện với từ khóa fact. Một sự kiện có thể có tên hoặc không có tên. fact [tên ] {khai báo các ràng buộc } Một sự kiện cũng giống như một ràng buộc bất biến trong lập trình hướng đối tượng. Nó tham chiếu tới đối tượng, buộc đối tượng phải giữ các ràng buộc trong toàn bộ quá trình tồn tại của nó. 16 2.2.3 Khai báo mệnh đề và chức năng – predicate & fuction. Trong mô hình Alloy[2] ngoài các ràng buộc bất biến kiểu sự kiện luôn luôn được thực thi thì còn một số ràng buộc chỉ thực thi khi được gọi đến hoặc được sử dụng lại trong mô hình đó chính là các ràng buộc thuộc nhóm mệnh đề - predicate và chức năng- function. Một chức năng là một biểu thức được đặt tên. Nó có tham biến, số lượng tham biến là tùy chọn. Và tùy chọn có kết quả trả về hay không. Chức năng trong Alloy[2] hoàn toàn có cấu trúc giống như chức năng trong các ngôn ngữ lập trình. Khai báo một chức năng bắt đầu với từ khóa func func [tên chức năng][danh sách tham biến]: [Kiểu dữ liệu trả về]{các ràng buộc} Một mệnh đề là một ràng buộc được đặt tên. Nó cũng có danh sách tham biến, số lượng tham biến là tùy chọn. Khi một mệnh đề được gọi đến thì một biểu thức phải cung cấp cho mỗi tham biến của mệnh đề có nghĩa là ràng buộc trong mệnh đề tương ứng với mỗi tham biến sẽ được thay thế bằng một biểu thức khởi tạo. Khai báo một mệnh đề bắt đầu với từ khóa pred pred[tên mệnh đề](danh sách tham biến) {Khai báo ràng buộc} 2.2.4 Khai báo khẳng định - assertion Một khẳng định - assertion là một ràng buộc. Một khẳng định tồn tại độc lập không phụ thuộc và các sự kiện, mệnh đề...Nhóm những ràng buộc khẳng định một điều gì đó được tập hợp lại vào một khẳng định. Đôi khi, trong mô hình một khẳng định dùng để kiểm tra một hoặc nhiều sự kiện. Kết quả thực hiện một khẳng định sẽ cho một trong 2 kết quả là tìm ra phản ví dụ cho khẳng định bên trong khẳng định được thực thi hoặc không tìm thấy phản ví dụ, điều này là rất có ích để kiểm tra tính toàn vẹn của mô hình. Trong mô hình có thể dùng nhiều khẳng định và các khẳng định được đặt tên. Khai báo khẳng định bắt đầu với từ khóa assert. assert [tên khẳng định] {các biểu thức ràng buộc } 2.2.5 Lệnh trong Alloy Trong Alloy[2] khi muốn phân tích mô hình chúng ta phải viết lệnh. Lệnh bắt đầu với từ khóa run thông báo cho bộ phân tích Alloy[2] tìm kiếm thực thể của một mệnh đề xác định. Lệnh bắt đầu với từ khóa check thông báo cho bộ phân tích tìm kiếm phản ví dụ cho một khẳng định xác định. Trong khi đưa ra các dòng lệnh chúng ta có thể đưa thêm vào phạm vi, phạm vi sẽ giới hạn số lượng các thể hiện phải có trong một mệnh đề hoặc là số lượng phản ví dụ. Để xác định chính xác phạm vi dòng lệnh thì cần thiết phải giới hạn cho mỗi ký hiệu . Việc thực hiện giới hạn cho ký hiệu cha cũng thỏa mãn giới hạn cho ký hiệu con. 17 2.2.6 Khai báo mô đun Alloy[2] cung cấp một hệ thống mô đun đơn giản nó cho phép chia một mô đun lớn thành nhiều mô đun nhỏ hơn và cũng tiện lợi trong việc tạo ra các thư viện riêng được đinh nghĩa trước đó. Mỗi mô đun tương ứng với một file. Mỗi mô đun biểu diễn bằng tên đường dẫn tương ứng với tên file trong hệ thống. Khai báo một mô đun bắt đầu với từ khóa module tiếp đến là tên đường dẫn. module đường_dẫn_mô_đun Mỗi mô đun muốn sử dụng một mô đun khác thì phải đính nó vào bằng cách sử dụng khai báo bắt đầu bằng từ khóa import và theo sau là đường dẫn tới file. import đường_dẫn_mô_đun Mô đun chính là không gian tên cho các khai báo bên dưới nó. Khi có 2 ký hiệu có tên giống nhau thì lúc này muốn sử dụng ký hiệu đó thì cần thêm vào trước đó không gian tên chính là tên đường dẫn mô đun. Thông thường thì mỗi đường dẫn mô đun sẽ có một biệt danh cho nó để tránh sự dài dòng trong trình bày. 2.2.7 Thực thi mô hình Alloy Trong phần trước chúng ta đã tìm hiểu các thành phần cơ bản của một mô hình Alloy[2] ký hiệu, sự kiện, trường, mệnh đề ... trong phần này chúng ta tìm hiểu cách thực thi mô hình tức là làm thế nào để đưa ra các thể hiện mô hình, hoặc tìm ra các thể hiện sai của mô hình. Alloy[2] cung cấp cho chúng ta công cụ phân tích tự động Alloy Analyzer, với sự giúp sức của công cụ sẽ đưa ra các thể hiện theo ý muốn của chúng ta một cách nhanh chóng và trực quan. Các thể hiện được tìm ra khi chúng ta thực thi dòng lệnh run. Thể hiện của mô hình là các cụ thể hóa của các ký hiệu với các trường - field và phải thỏa mãn các ràng buộc trong sự kiện. Chỉ những ký hiệu được chỉ rõ trong sự kiện thì mới cần phải thỏa mãn sự kiện đó, điều này tương tự như từ khóa context trong OCL[5], sẽ chỉ ra đối tượng nào được chỉ ra trong ngữ cảnh- context đó thì mới cần tuân thủ các biểu thức OCL[5] được khai báo trong đó. 2.3 Công cụ Alloy Analyzer Từ phiên bản đầu tiên được phát hành kèm theo bộ phân tích Alloy Analyzer[6], đến thời điểm hiện tại Alloy[2] đang là phiên thứ 4 và kèm theo nó là bộ phân tích Alloy Analyzer[6] phiên bản thứ 4. Bộ phân tích Alloy Analyzer[6] là một công cụ mạnh mẽ sử dụng để tìm kiếm tất cả thể hiện của một mô hình được đặc tả trong mô hình Alloy[2]. Bằng cách thức chạy một mệnh đề (run mệnh đề), bộ phân tích Alloy Analyzer[6] sẽ tìm kiếm tất cả thể hiện mô hình thỏa mãn các ràng buộc mô hình hoặc bộ phân tích Alloy Analyzer[6] sẽ tìm các thể hiện là phản ví dụ của đặc tả mô hình khi chay lệnh check 18 Bộ cài đặt : bao gồm Alloy Analyzer tải về từ địa chỉ và bộ cài JDK 1.5 trở lên tại Giao diện chính của bộ phân tích Alloy Analyzer[6] Hình 2. Công cụ Alloy Analyzer “Sử dụng công cụ cung cấp cho chúng ta các tùy chọn cho việc trình diễn thể hiện mô hình như : dạng cây thư mục, dạng siêu dữ liệu XML hay dạng Visualsation là dạng biểu diễn đồ họa của mô hình”[6]. 2.4 Ví dụ đặc tả Alloy Đặc tả danh sách địa chỉ. Mô tả phi hình thức ContactBook là một cuốn danh bạ địa chỉ các cá nhân trong đó có: Tên ,địa chỉ (nơi làm việc và nhà riêng), số điện thoại (di động, và cố định), địa chỉ mail, Các ràng buộc : Không được viết tên, địa chỉ của cùng một người nhiều lần Các chức năng : Thêm, sửa, xóa một người theo tên 19 Đặc tả Alloy Thể hiện của mô hình bao gồm các ký hiệu và thỏa mãn các ràng buộc trong sự kiện. Rõ ràng nếu chỉ sử dụng UML[1] thì chúng ta không thể biểu diễn được các ràng buộc nói trên. Trong khi đó đặc tả ràng buộc cho ví dụ trên bằng Alloy[2] thì ngắn gọn và dễ dàng. Kết quả Contact là ký hiệu ảo, nó có các trường mail - địa chỉ hòm thư, addr - địa chỉ nhà, mobile – số điện thoại, và tele – số điện thoại cố đinh. Mỗi một Contact đều có đủ các trường trên. Các ký hiệu Name và Address đều kế thừa từ ký hiệu ảo Contact. Contacts là một ký hiệu trong đó chỉ có một trường biểu diễn quan hệ giữa hai ký hiệu Name và Address. Ràng buộc được đưa vào buộc các thể hiện Name, Contact thỏa mãn rằng mỗi thể hiện của Name chỉ xuất hiện trong Contacts – Danh bạ một lần và trong Contacts – Danh bạ không có trường hợp các trường mail, addr, mobile, tele xuất hiện hai lần trong đó. 20 Hình 3. Kết quả thực thi mô hình Alloy Kết quả thực thi mệnh đề : “thêm địa chỉ” –addContact Mệnh đề thêm địa chỉ được biểu diễn trong Alloy[2] như sau. Đầu vào của mệnh đề là các biến có kiểu Contacts, Name, Address. Chúng ta định nghĩa rằng việc thêm vàm địa chỉ tức là ta có một Contacts mới và Contacts mới chính là Contacts cũ thêm với địa chỉ muốn thêm vào. Hình 4. Kết quả thực thi mệnh đề "thêm” Chương 3 . Chuyển đổi biểu đồ lớp với đặc tả OCL sang mô hình Alloy 21 Phần trước chúng ta đã biết Alloy[2] là một ngôn ngữ mô hình hóa dựa trên logic vị từ bậc nhất. Alloy[2] cung cấp các khai báo trừu tượng, các khai báo thừa kế. Cả UML[1] và Alloy[2] đều làm việc trên tư tưởng hướng đối tượng. Do đó việc chuyển đổi giữa Alloy[2] và biểu đồ lớp UML[1] là có thể và đảm bảo ý nghĩa được bảo toản. Ngoài ra, Alloy[2] cũng rất thích hợp trong việc biểu diễn các ràng buộc bởi vì nó dựa trên logic vị từ bậc nhất do vậy việc chuyển các biểu thức OCL[5] sang Alloy[2] cũng hoàn toàn là có thể.Hơn thế nữa công cụ phân tích cho Alloy[2] cũng rất mạnh. Dựa vào công cụ Alloy Analyzer chúng ta có thể trong một thời gian ngắn tìm được ra những thể hiện của mô hình hoặc kiểm tra độ chính xác của mô hình Alloy[2] ở các mức độ khác nhau bằng cách đưa ra các loại ràng buộc sự kiện hoặc mệnh đề hoặc khẳng định. Trong thực tế Alloy[2] đã được sử dụng trong việc kiểm chứng, các vấn đề đòi hỏi những ràng buộc phức tạp, độ chính xác cao được chuyển thành các mô hình trong Alloy[2], sau đó các mô hình được kiểm chứng thông qua công cụ Alloy Analyzer. Một biểu đồ lớp UML[1] với những đặc tả OCL[5] sau khi chuyển được sang mô hình Alloy[2] sẽ rất có lợi trong việc đưa ra các mô hình đối tượng là một thể hiện cụ thể của biểu đồ lớp. Ngoài ra còn có lợi trong việc kiểm chứng tính đúng đắn của biểu đồ lớp bằng cách đưa ra các phản ví dụ là thể hiện cụ thể của biểu đồ lớp vi phạm các ràng buộc OCL[5]. Như vậy, với những kiến thức đã tìm hiểu về biểu đồ lớp UML[1], đặc tả OCL[5] cho biểu đồ lớp, Alloy[2] và công cụ Alloy Analyzer. Chúng ta cũng đã làm rõ sự cần thiết chuyển đổi biểu đồ lớp UML[1] với đặc tả OCL[5] sang Alloy[2]. Khi tiến hành chuyển đổi chúng ta sẽ chuyển các yếu tố của mô hình UML[1] sang các yếu tố tương ứng trong mô hình Alloy[2] để đảm bảo tương ứng ngữ nghĩa. Dưới đây là mô hình thực hiện việc chuyển đổi. 22 Hình 5. Mô hình chuyển đổi biểu đồ lớp với đặc tả OCL sang mô hình Alloy Mô hình chuyển đổi sẽ có các bước: Bước thứ nhất : Chuyển biểu đồ lớp UML[1] với các liên kết phức tạp (kết tập, hợp thành, tổng quát hóa,..) sang biểu đồ lớp với các liên kết đơn giản hơn. Bước thứ hai : Chuyển biểu đồ lớp UML[1] nhận được từ bước thứ nhất sang mô hình Alloy[2]. Bước thứ ba : Chuyển các đặc tả OCL[5] sang ràng buộc Alloy[2]. Sau khi thực hiện bước thứ ba, lúc này chúng ta có thể sử dụng kết quả của bước này thông qua công cụ Alloy Analyzer[6] để đưa ra các thể hiện mô hình. 3.1 Chuyển biểu đồ lớp UML với các liên kết phức tạp sang biểu đồ lớp UML với các liên kết đơn giản Mục đích của việc chuyển đổi biểu đồ lớp với các liên kết phức tạp sang biểu đồ lớp UML[1] với các liên kết đơn giản hơn để làm đơn giản hơn việc chuyển đổi biểu đồ lớp UML[1] sang mô hình Alloy[2] mã vẫn đảm bảo ngữ nghĩa mô hình tương đương. Thay vì chuyển đổi một biểu đồ lớp UML[1] với các liên kết phức tạp như quan hệ kết tập, hợp thành, tổng quát hóa chúng ta sẽ chỉ phải chuyển các biểu đồ lớp UML[1] với chỉ các liên kết nhị phân. Trong quá trình chuyển đổi này chúng ta sẽ đưa thêm vào các biểu thức OCL[5] để đảm bảo sự tương đương về ngữ nghĩa giữa biểu đồ lớp UML[1] trước khi chuyển và biểu đồ lớp UML[1] sau khi chuyển. 23 3.1.1 Quan hệ nhị phân với các lượng từ Hình 6. Chuyển quan hệ nhị phân với lượng từ[3] Vế trái của hình vẽ trên biểu diễn liên kết nhị phân giữa 2 lớp với lượng từ tham gia. Vế phải là biểu diễn nhị phân của 2 lớp, nhưng lúc này ta không quan tâm tới lượng tử tham gia của 2 lớp trong mối liên hệ. Giải thích viết tắt cho hình 6. ra : Tên vai trò của Class B với Class A, ra : B -> set A rb : Tên vai trò của Class A với Class B, rb : A->set B la..ha : Với một đối tượng là thể hiện của Class B thì số lượng đối tượng của Class A liên hệ với nó trong đoạn từ la đến ha tương tự như vậy với lb..hb. Cả ra, rb đều được gọi với thuật ngữ chung là mút liên kết -association end . Biểu diễn ràng buộc bằng OCL Như đã thấy trong Hình 8 để vế trái và vế phải tương đương nhau thì ta phải thêm vào vế phải ràng buộc OCL[5]. Ràng buộc được đưa ra nhằm biểu diễn ràng buộc về số lượng la..ha và lb..hb thành các ràng buộc OCL[5]. Ràng buộc OCL được thêm vào Ràng buộc tương đương trong Alloy A->forAll(a | a.rb->size >= lb and a.rb- >size forAll(b | b.rb- >size>=la and b.rb->size <= ha)[4] all a : A | #a.rb >=lb and #a.rb <=hb all b: B | #b.ra >=la and #b.ra <=ha Các ràng buộc sẽ được đặt trong các sự kiện trong Alloy[2], điều đó đảm bảo các ràng buộc sẽ luôn luôn được tham chiếu trong suốt quá trình thực thi chương trình. Ví dụ Mô tả : Giả sử chúng ta có liên kết nhị phân giữa 2 lớp Student và Teacher. 24 Hình 7. Ví dụ chuyển quan hệ nhị phân với lượng từ Sau khi chuyển thì lúc này chúng ta không cần quan tâm tới lượng từ tham gia liên kết của 2 lớp nữa. Dưới đây chúng ta sẽ chuyển vế phải của Hình 9 sang biểu diễn Alloy[2]. Ở đây mỗi một lớp chuyển thành một ký hiệu trong Alloy[2], các ràng buộc OCL[5] chuyển tương ứng thành các biểu thức logic Alloy[2]. Bảng 4. Chuyển đặc tả OCL của lớp Student sang Alloy UML[1] và đặc tả OCL Biểu diễn Alloy class Student sig Student class Teacher sig Teacher Student->forAll(s | s.study->size >=5 and s.study->size <=10) and Teacher->forAll(t | t.teach->size >=25 and t.teach->size <=50) all s : Student | #s.study >=5 and #s.study <=10 all t : Teacher | #t.teach >=25 and t.teach <=50 study : Student -> set Teacher chuyển thành một trường trong sig Student teach : Teacher -> set Student chuyển thành một trường trong sig Teacher 25 Biểu diễn đặc tả Alloy Hình 8. Đặc tả Alloy lớp Student 3.1.2 Chuyển quan hệ tổng quát hóa sang quan hệ nhị phân Hình 9. Chuyển quan hệ tổng quát hóa sang quan hệ nhị phân[3] Mô tả : Vế trái Hình 9 biểu diễn quan hệ tổng quát hóa giữa 2 lớp S và G trong đó lớp G là lớp tổng quát hóa, vế phải biểu diễn quan hệ nhị phân giữa 2 lớp S và G và thêm vào đó các lượng tử tham gia quan hệ và ràng buộc. Giải thích Hình 9 rg : Biểu diễn mút liên hệ (association end) giữa 2 lớp S và G và biểu diễn rg : S-> G. Ràng buộc : 26 Chúng ta phải đưa ra ràng buộc để đảm bảo tương đương ngữ nghĩa giữa vế trái và vế phải của hình. Ràng buộc thêm vào đảm bảo một đối tượng của lớp S buộc phải liên hệ với một đối tượng G duy nhất hay là sẽ không có 2 đối tượng thuộc lớp S cùng liên hệ với một đối tượng thuộc lớp G. Biểu diễn ràng buộc bằng OCL S->forAll(s,s’ | ss’ implies s.rg s’.rg ) Ví dụ Mô tả : Giả sử có 2 lớp G và lớp S, trong đó lớp G là lớp tổng quát hóa của lớp S. Lớp G có thuộc tính name kiểu string. Lớp S có thêm thuộc tính old kiểu Old. Mục đích của chúng ta là chuyển quan hệ tổng quát hóa giữa 2 lớp S và G thành quan hệ nhị phân như trình bày ở trên. Hình 10. Ví dụ mô hình chuyển đổi OCL sang Alloy Chuyển vế phải của hình 12 sang biểu diễn Alloy[2]. Mỗi lớp chuyển thành một khai báo ký hiệu trong Alloy[2], mỗi thuộc tính lớp chuyển thành một trường trong ký hiệu tương ứng, mỗi mút liên kết cũng chuyển thành một trường quan hệ trong ký hiệu tương ứng, các ràng buộc OCL[5] chuyển thành các biểu thức ràng buộc logic Alloy[2]. Kiểu của thuộc tính chuyển thành một khai báo ký hiệu. Bảng 5. Quy tắc chuyển quan hệ tổng quát hóa sang quan hệ nhị phân UML và đặc tả OCL Biểu diễn Alloy tương ứng class S sig S Kiểu dữ liệu Old sig Old Thuộc tính old một trường old trong sig S Class G sig G 27 Kiểu dữ liệu string sig string thuộc tính name một trường name trong sig G rg chuyển thành trường trong S ràng buộc OCL : S->forAll(s,s’ | s s’ implies s.rg s’.rg) all s,s’: S | s!= s’ => s.rg != s’.rg và đảm bảo một đối tượng của lớp S chỉ liên hệ với một đối tượng của lớp G. Biểu diễn đặc tả OCL Bên cạnh việc chuyển quan hệ tổng quát hóa hay còn gọi là quan hệ kế thừa trong ngôn ngữ lập trình hướng đối tượng sang quan hệ nhị phân thì chúng ta có thể sử dụng quan hệ kế thừa trong Alloy[2], mỗi lớp trong biểu đồ UML[1] chuyển thành một ký hiệu trong Alloy[2], quan hệ tổng quát hóa biểu diễn trong UML[1] chuyển trực tiếp thành quan hệ kế thừa trong Alloy[2] thông qua cú pháp : sig G{} sig S extends sig G {} Trong đó : G là lớp tổng quát hóa của lớp S. Tổng quát lại quy tắc chuyển đổi đã nêu ở phần 3.1.1 và 3.1.2 chúng ta có quy tắc chuyển đơn giản sau Tên vai trò - role name : Tên vai trò thể hiện vai trò của một lớp với lớp khác, chúng sẽ được chuyển thành các trường quan hệ trong khai báo của ký hiệu tương ứng. Bản số quan hệ -muliticity: Bản số cho biết một đối tượng của lớp này có thể liên hệ với bao nhiêu đối tượng của lớp kia. Bản số quan hệ sẽ được chuyển thành các khai báo bất biến trong OCL[5], tiếp đó các bất biến này được chuyển thành các khai báo logic 28 Alloy[2] và được đặt trong khai báo sự kiện, khai báo này tương đương với khai báo bất biến trong OCL[5], các ràng buộc trong sự kiện luôn luôn được tham chiếu trước tiên khi thực thi chương trình. Tổng quát hóa : Có 2 cách có thể biểu diễn quan hệ này trong Alloy[2], với cách thứ nhất chúng ta sẽ chuyển quan hệ tổng quát hóa sang quan hệ nhị phân bình thường và thêm vào các ràng buộc cho quan hệ, cách thứ 2 chúng ta biểu diễn trực tiếp quan hệ tổng quát hóa trong biểu diễn UML[1] sang quan hệ kế thừa trong Alloy[2] thông qua từ khóa extends. 3.1.3 Chuyển quan hệ kết tập và tạo thành sang quan hệ nhị phân Quan hệ kết tập – Aggregation[1] là dạng đặc biệt của liên kết Association[1], quan hệ kết tập biểu diễn mối quan hệ giữa toàn thể - whole và bộ phận – part. Ràng buộc cho toàn thể - whole chỉ có thể tồn tại khi các bộ phận của nó tồn tại. Quan hệ tạo thành – Composition[1] là dạng đặc biệt của quan hệ kết tập. Quan hệ tạo thành còn thêm ràng buộc cho bộ phận – part, bộ phận chỉ tồn tại bên trong một toàn thể, hay là bộ phận không thể tồn tại ngoài toàn thể. Ngoài ra quan hệ tạo thành còn ràng buộc chia sẻ bộ phận – part tức là, nếu có 2 toàn thể cùng chứa bộ phận như nhau thì 2 toàn thể đó phải trùng nhau. Mô hình chuyển đổi ở đây là từ quan hệ kết tập và tạo thành chuyển sang quan hệ nhị phân và thêm vào quan hệ nhị phân các ràng buộc logic Alloy[2]. Áp dụng quy tắc phần 3.1.1 để chuyển quan hệ nhị phân sang quan hệ trong Alloy[2]. Giải thích hình vẽ: A: Lớp toàn thể - aggregate P : Lớp bộ phận – part rp: Tên vai trò của lớp A đối với lớp P, và rp được biểu diễn rp: A -> set P Ràng buộc Quan hệ kết tập Quan hệ tạo thành 29 Ràng buộc cho toàn thể fact {all a: A | some p: P | p in a.rp} fact {all a: A | some p: P | p in a.rp} Ràng buộc cho bộ phận fact {all p: P | some a: A | p in a.rp} Ràng buộc chia sẻ bộ phận fact {all p: P | some a,a’: A | p in a.rp and p in a’.rp implies a = a’ } 3.1.4 Chuyển các thành phần của lớp sang Alloy Trong các phần 3.1.1, 3.1.2 và 3.1.3 chúng ta đã xem xét và đưa ra cách thức để biểu diễn quan hệ giữa các lớp trong biểu đồ lớp UML[1] sang biểu diễn trong Alloy[2], tuy nhiên các biểu đồ lớp ở trên mới chỉ chứa các lớp được mô tả ở mức khái niệm, các lớp không có thuộc tính, phương thức...Trong phần này sẽ đưa ra cách thức chuyển từng thành phần trong một lớp sang biểu diễn Alloy[2]. Ngoài ra cũng đưa ra cách thức chuyển các kiểu enum sang biểu diễn Alloy[2].  Lớp Mỗi một lớp sẽ được khai báo thành một ký hiệu trong Alloy[2], lớp ảo sẽ được chuyển thành một ký hiệu ảo. Tên lớp chuyển thành tên ký hiệu tương ứng. Hình 11. Chuyển lớp sang ký hiệu Cú pháp biểu diễn ký hiệu : Bắt đầu với từ khóa sig (giống như bắt đầu với từ khóa class), tiếp đến là tên của class tương ứng trong lớp UML[1] . Biểu diễn class Student tương ứng với biểu diễn. 30 Các thuộc tính của lớp sẽ thành các trường được khai báo trong cặp “{}”.  Thuộc tính của lớp Sau khi chuyển một lớp sang một ký hiệu, tiếp đến chúng ta chuyển các thuộc tính của lớp thành các trường trong ký hiệu trong cặp “{}” của ký hiệu tương ứng. Mỗi thuộc tính trong lớp được biểu diễn trong biểu đồ UML[1] với cú pháp tên_thuộc _tính : kiểu_dữ_liệu Tương đương như vậy trong Alloy[2] cũng sẽ là: tên_trường (chính là tên thuộc tính của lớp) : kiểu_dữ_ liệu Các trường trong Alloy[2] được phân cách nhau bởi dấu phẩy “,”. Trong Alloy[2], chỉ hộ trợ 1 số kiểu dữ liệu nguyên thủy. Do vậy, đối với các kiểu dữ liệu của thuộc tính không nằm trong kiểu dữ liệu hỗ trợ của Alloy[2] thì chúng ta sẽ phải tự định nghĩa kiểu dữ liệu đó bằng cách chuyển kiểu dữ liệu đó thành một khai báo ký hiệu. Lớp với thuộc tính Ví dụ trong hình vẽ trên lớp Student có thuộc tính birthday có kiểu dữ liệu Date không được hộ trợ trong Alloy[2] thì chúng ta phải định nghĩa kiểu dữ liệu trên như dưới đây sig Date {day : Int,mont : Int, year : Int} Các trường phân cách nhau bởi dấu phẩy. Và khi đó biểu diễn của lớp Student trong Alloy[2] sẽ đơn giản như sau : sig Student {birthDay : Date} 31  Phương thức của lớp Trong biểu diễn lớp của UML[1], các phương thức được biểu diễn với cú pháp : Kiểu_Trả_về Tên_Phương_thức [biến_1 : Kiểu_của_biến1, biến 2: Kiểu_biến2] {} Kiểu trả về có thể là kiểu void, hoặc một kiểu bất kỳ nào đó, danh sách tham biến là tùy chọn tức là tồn tại các phương thức không có danh sách tham biến. Đến đây chúng ta có 2 cách đều có thể lựa chọn, lựa chọn thứ nhất đối với các phương thức không trả về kết quả (trả về kiểu void) sẽ chuyển thành khai báo mệnh đề trong Alloy[2], lựa chọn thứ hai chuyển các phương thức thành khai báo chức năng trong Alloy[2]. Với cả 2 lựa chọn thì tên phương thức chuyển thành tên mệnh đề hoặc chức năng tùy theo lựa chọn. Danh sách các tham biến và kiểu của chúng được chuyển thành danh sách tham biến của mệnh đề hoặc chức năng tùy theo cách lựa chọn. Như đã đề cập ở phần trước, Alloy[2] chỉ cung cấp một số kiểu dữ liệu là integer ..., do vậy với những kiểu của biến trong danh sách tham biến không nằm trong 2 kiểu của Alloy[2] thì sẽ cần khai báo kiểu của biến đó là một ký hiệu. Giả sử chúng ta có 1 class A với phương thức được khai báo như ở dưới. void operation (para1 : Type1, para2 : Type2) Trong phần trước chúng ta đã đề cấp cách chuyển lớp thành một ký hiệu, các thuộc tính thành các khai báo trường trong ký hiệu tương ứng, tuy nhiên vấn đề là trong khai báo ký hiệu không có khai báo mệnh đề hay chức năng, tất cả khai báo này nằm ngoài ký hiệu. Do đó khi khai báo mệnh đề hay chức năng phải chỉ rõ ký hiệu của nó. Với phương thức operation ở trên chúng ta sẽ chuyển như sau: void operation (para1 : Type1, para2 : Type2) {}-> pred A::operation[para1: Type1, para2 : Type2] {} Đối với phương thức có kết quả trả về typeReturn operation(para1 : Type1, para2 : Type2){} -> 32 fun A::operation[para1 : Type1, para2 : Type2]:typeReturn {} Ví dụ : Cho lớp Student với các đặc tả Hình 12. Lớp với thuộc tính, phương thức và đặc tả OCL Biểu diễn lớp tương ứng trong Alloy : 3.1.5 Chuyển các ràng buộc bất biến, tiền điều kiện hậu điều kiện OCL Sự khác biệt OCL[5] và Alloy[2] không cho phép chuyển đổi giữa chúng một cách hoàn toàn. Do vậy chúng ta chỉ đề cập tới một số khía cạnh có thể chuyển đổi từ OCL[5] sang Alloy[2]. Bảng sau mô tả phép chuyển. Các ký hiệu viết tắt col : Biểu diễn một tập hợp – collection trong OCL 33 v : Biến – varable (v) trong biểu thức T : Biểu diễn kiểu của biến be : Biểu diễn biểu thức Boolean e : Biểu diễn biểu thức Bảng 6. Quy tắc chuyển OCL sang Alloy – [4] OCL Alloy col ->forAll(v : T | be) all Tr(v) : Tr(col) | Tr(be) col -> exists(v : T | be) some Tr(v) : Tr(col) | Tr(be) e1 and e2 Tr(e1) && Tr(e2) not e !Tr(e) col -> size() #Tr(col) col -> includes(v : T) Tr(v) in Tr(col) col -> excludes(v : T) Tr(v) ! in Tr(col) col1 -> includesAll(col2) Tr(col2) in Tr(col1) col1 -> excludesAll(col2) Tr(col2) ! in Tr(col1) col -> including(v :T) Tr(col) + Tr(v) col -> excluding(v: T) Tr(col) – Tr(v) col ->isEmpty() no ( col) col ->notEmpty() some (col) if condition then e1 else e2 Tr(condition) =>Tr(e1) else Tr(e2) e.oclIsUndefined #Tr(e) = 0 e -> oclKindOf(v : T) Tr(v) in Tr(e) col1 -> union(col2) Tr(col1) + Tr(col2) col1 -> intersection(col2) Tr(col1) & Tr(col2) 34 col1 ->product(col2) Tr(col1) -> Tr(col2) col->sum() sum Tr(col) Ràng buộc OCL[5] đặc tả biểu đồ UML[1] chúng ta chỉ đề cập tới 2 vấn đề. Vấn đề thứ nhất chuyển các đặc tả bất biến OCL[5] sang biểu thức logic Alloy[2] và vấn đề thứ hai chuyển đặc tả tiền điều kiện và hậu điều kiện của một phương thức sang biểu thức logic Alloy[2].  Bất biến Mỗi bất biến đặc tả OCL[5] được hiểu là ràng buộc cho mọi thể hiện của đối tượng được khai báo trong một ngữ cảnh cụ thể. Do vậy chúng ta sẽ chuyển các bất biến thành các biểu thức ràng buộc Alloy[2] nằm trong sự kiện, và chỉ rõ đối tượng chịu ràng buộc trong sự kiện. Ví dụ với đặc tả lớp Student chúng ta khai báo thuộc tính years (sinh viên năm thứ mấy), giả sử chúng ta có ràng buộc là mọi sinh viên phải là sinh viên năm thứ 1, hoặc 2 ..4. Lớp với thuộc tính và phương thức. Biến seft chỉ các thể hiện của đối tượng Student. Do vậy trong sự kiện chúng ta phải chỉ ra đối tượng Student. Do vậy bất biến này sẽ được viết thành biểu thức logic trong Alloy[2] như sau: fact {all s : Student | int s.years >=1 and int s.years <=4 } all s : Student  Chỉ ra tất cả thể hiện của đối tượng Student. int s.years >=1 and int s.years <=4  Ràng buộc cho thể hiện đối tượng.  Tiền điều kiện, hậu điều kiện của một phương thức. 35 Phần trước chúng ta đã đề cập tới chuyển một phương thức của biểu đồ lớp UML[1] sang Alloy[2]. Khi chuyển một tiền điều kiện và hậu điều kiện của một phương thức trước tiên chúng ta chuyển phương thức đó sang Alloy[2]. Các tiền điều kiện là các điều kiện cho các tham biến, khi đó chúng ta chỉ việc thêm vào các ràng buộc cho các biến trong phương thức được chuyển sang Alloy[2], còn các hậu điều kiện chính là kiểm tra kết quả sau khi thực thi phương thức chúng ta chỉ cần cho biến có kiểu trả về thỏa mãn ràng buộc OCL[5]. Ví dụ chúng ta có phương thức operation(pre : T) và ràng buộc tiền điều kiện là pre > 5 và ràng buộc hậu điều kiện là post < 10. operation(pre : T)  pre operation(pre : T, post : T’) {pre > 5 & post < 10} Tuy vậy việc chuyển các biểu thức hậu điều kiện là tương đối phức tạp. Do vậy trong đây chúng ta chỉ chuyển đổi các biểu thức tiền điều kiện. 3.2 Những vấn đề khi chuyển đổi Mặc dù cả UML[1] và Alloy[2] được thiết kế để mô tả mô hình hướng đối tượng, tuy nhiên UML[1] và Alloy[2] có một số điểm khác biệt trong cách tiếp cận một số khái niệm trong hướng đối tượng ví dụ như cách tiếp cận trong vấn đề thừa kế, ghi đè...do vậy ảnh hưởng tới việc chuyển đổi giữa mô hình UML[1] sang Alloy[2].  Vấn đề thừa kế[4] Cả UML[1] và Alloy[2] đều cung cấp khái niệm thừa kế. Trong UML[1], một lớp con thừa kế từ một hoặc nhiều lớp. UML[1] sử dụng khái niệm “redefine” để thể hiện những thuộc tính hoặc phương thức bị ghi đè ở lớp con. Trong khi đó, một ký hiệu trong Alloy[2] có thể được kế thừa từ một ký hiệu khác và thành phần của ký hiệu là tập con của ký hiệu cha và một ký hiệu con không thể khai báo một trường có tên trùng với tên trường đã có trong lớp cha tức là việc ghi đè trực tiếp trong Alloy[2] là không cho phép.  Không gian tên[4] Mọi thành phần mô hình trong UML[1] đều được định nghĩa trong một không gian tên. Ví dụ như, các lớp trong mô hình UML[1] được đặt trong một không gian tên của gói và các thuộc tính của lớp thì được đặt trong không gian tên của lớp nó thuộc về. Trong khi đó, mọi thành phần trong Alloy[2] đều thuộc về một không gian tên mô đun. Ví dụ như trong đặc tả UML[1] có định nghĩa :”Tập hợp tên của thuộc tính và tên của lớp không cần thiết phải tách rời”. Nhưng trong Alloy[2], tên của ký hiệu có sự tách rời với tên các trường của nó. Chính vì thế trong khi chuyển đổi chúng ta phải chắc chắn tên duy nhất được tạo ra cho mỗi thành phần của Alloy[2] trong cùng một không gian tên mô-đun.  Kiểu được định nghĩa trước[4] Đặc tả UML[1] định nghĩa trước một số kiểu dữ liệu nguyên thủy như (String, Real, Integer...) 36 Trong khi đó, Alloy[2] có một hệ thống kiểu rất đơn giản và chỉ duy nhất kiểu Integer là kiểu dữ liệu nguyên thủy được định nghĩa trước. Ví dụ như kiểu dữ liệu String được đinh nghĩa trước trong UML[1] nhưng không được đinh nghĩa trong Alloy[2], cách tiếp cận cho các vấn đề này là chúng ta khai báo một ký hiệu kiểu String trong mô hình.  Kết tập và tạo thành[4] Trong UML[1] cả kết tập và tạo thành là dạng đặc biệt của liên hệ giữa hai lớp. Alloy[2] không hỗ trợ trực tiếp hai kiểu quan hệ kết tập và tạo thành. Đây là khó khăn khi chuyển đổi biểu đồ lớp với các quan hệ kết tập và tạo thành trong Alloy[2]. Trong khóa luận của mình em có đưa ra cách thức chuyển đổi hai quan hệ trên sang đặc tả Alloy[2] trong phần chương 4.  Mô hình tĩnh và mô hình động[4] Mô hình trong Alloy[2] là mô hình tĩnh. Một mô hình trong Alloy[2] định nghĩa các thể hiện của hệ thống thỏa mãn các ràng buộc. Bản thân Alloy[2] không chứa đựng trong nó khái niệm về trạng thái của hệ thống. Trong khi đó UML[1] sử dụng khái niệm tĩnh để biểu diễn quan hệ cấu trúc giữa các thành phần của hệ thống thông qua các ràng buộc, các đặc tả phương thức với sự thêm vào các điều kiện như tiền điều kiện và hậu điều kiện của phương thức. Một mô hình hệ thống tĩnh được chỉ ra tại một thời điểm thông qua các giá trị của đối tượng, thuộc tính các liên kết giữa các thành phần trong mô hình hệ thống. Một giải pháp cho vấn đề này là sử dụng mẫu mô hình động trong Alloy[2] để giải quyết vấn đề trên. Với cách này chúng ta có thể mô tả được giá trị tiền điều kiện của mỗi phương thức ở trạng thái đầu và mô tả giá trị hậu điều kiện của mỗi phương thức ở trạng thái tiếp theo. 3.3 Kết luận. Như vậy, trong chương 3, em đã trình bày về mô hình chuyển đổi, các quy tắc chuyển đổi giữa các yếu tố của mô hình UML[1] sang các yếu tố mô hình Alloy[2] và các quy tắc chuyển giữa OCL[5] sang Alloy[2]. Cụ thể là các quy tắc chuyển đổi một lớp, các thành phần của lớp sang đặc tả Alloy[2], thể hiện được liên kết nhị phân, các quan hệ kết tập, tạo thành, tổng quát hóa trong biểu diễn biểu đồ lớp UML[1] sang biểu diễn Alloy[2] bằng cách đưa thêm các ràng buộc Alloy[2] logic. Bên cạnh đó, trong chương này còn đề cập tới vấn đề hạn chế khi chuyển đổi từ mô hình UML[1] sang mô hình Alloy[2], có những hạn chế do khách quan và có những yếu tố chủ quan của con người. Trong chương 4, em sẽ trình bày bài toán minh họa áp dụng cho các quy tắc chuyển đổi mà đã nêu trong chương 3. 37 Chương 4 . Kiểm tra đặc tả hệ thống quản lý các tài khoản và các giao dịch trên máy ATM 4.1 Yêu cầu của hệ thống 4.1.1 Yêu cầu chức năng Hệ thống ATM cung cấp các chức năng chính sau:  Cho phép thao tác với các tài khoản như : thêm, xóa, sửa tài khoản  Cho phép thực hiện các chức năng giao dịch: Rút tiền, gửi tiền, xem thông tin tài khoản. 4.1.2 Ràng buộc cho hệ thống Hệ thống ATM đòi hỏi các ràng buộc sau:  Một máy ATM chỉ có duy nhất các yếu tố sau: màn hình, bàn phím, khe rút tiền.  Tất cả các tài khoản đều nằm trong một cơ sở dữ liệu của ngân hàng. Một tài khoản cụ thể được lưu trữ trong một cơ sở dữ liệu ngân hàng, tức là không tồn tại 2 cơ sở dữ liệu ngân hàng cùng lưu trữ thông tin về một tài khoản cụ thể.  Tại một thời điểm, chỉ có một giao dịch diễn ra.  Hai tài khoản khác nhau thì mã pin và mã cá nhân phải khác nhau.  Mọi tài khoản cụ thể có 2 thông số : tổng số tiền và số tiền có thể sử dụng. Tổng số tiền trong một tài khoản luôn luôn lớn hơn hoặc bằng số tiền có thể sử dụng. Tổng số tiền trong tài khoản nhỏ nhất bằng số dư tài khoản phải có. 38 4.2 Thiết kế cơ sở dữ liệu 4.2.1 Biểu đồ lớp Hình 13. Biểu đồ lớp hệ thống ATM[8] 4.2.2 Các ràng buộc được mô tả bằng OCL Hình 14. Ràng buộc OCL của hệ thống 39 Hình 14 mô tả ràng buộc OCL[5] bên trái và tương đương là đặc tả trong Alloy[2] bên phải. Ràng buộc OCL[5] được mô tả ở đây là ràng buộc cho quan hệ tạo thành giữa 2 lớp Account và lớ BankDatabase. 4.3 Chuyển đổi mô hình thiết kế sang Alloy Lớp ATM: Chuyển đổi lớp ATM sang đặc tả Alloy Hình 15. Đặc tả Alloy của lớp ATM Lớp ATM được chuyển thành khai báo ký hiệu trong Alloy, mỗi thuộc tính của lớp ATM được chuyển thành một trường nằm trong ký hiệu ATM của Alloy. Đối với kiểu của thuộc tính trong lớp ATM thì : Với kiểu dữ liệu được Alloy hỗ trỡ integer thì tất các các kiểu dữ liệu của các thuộc tính khác được khai báo thành các ký hiệu. Trong biểu đồ lớp, lớp ATM tham chiếu tới các lớp BankDatabase,..Screen, Keypad do vậy trong phần thuộc tính của ATM sẽ có các thuộc tính có kiểu là kiểu của các lớp nêu trên. Chúng ta quan sát rằng bản số quan hệ của ATM và BankDatabase, Screen, Keypad đều là 1. Bản số này được biểu diễn thành khai báo hạn định cho trường, chúng ta thấy rằng trong ký hiệu ATM thì hạn định cho các trường là một. 40 Lớp ATM có 3 phương thức. Ba phương thức này được chuyển hoàn toàn thành các mệnh đề - predicate. Danh sách tham biến của các phương thức trong biểu đồ lớp được mang nguyên vẹn thành danh sách tham biến của mệnh đề trong Alloy. Tương tự như vậy đối với các lớp khác. Lớp Account: Chuyển đổi đặc tả lớp Account sang biểu diễn Alloy Hình 16. Đặc tả Alloy của lớp Account Đặc tả ràng buộc hệ thống trong Alloy Đối với mọi thể hiện của Account phải thỏa mãn totalBalance lớn hơn avaiableBalance và totalBalance >5. Ngoài ra, với mọi thể hiện Account cũng phải thỏa mãn : Không có 2 thể hiện nào của Account trùng mã pin và accountNumber 41 Hình 17. Ràng buộc cho hệ thống ATM Kết quả thực thi mô hình 42 Kết luận Trong quá trình thực hiện đề tài Khóa luận tốt nghiệp, em đã tìm hiểu ngôn ngữ UML[1], OCL[5] và các công cụ hỗ trợ đặc tả UML[1] hiện nay. Em cũng đã tìm hiểu các phương pháp để kiểm tra các yếu tố mô hình UML[1] và tập trung vào phương pháp chuyển đổi mô hình UML[1] sang đặc tả Alloy[2] để có thể sử dụng công cụ Alloy Analyzer trong việc phân tích tự động các yếu tố của mô hình. Em đã đặc tả “hệ thống quản lý các tài khoản và các giao dịch ” để minh họa cho phương pháp này. Qua quá trình thực hiện khóa luận, em đã nắm được cách thức đặc tả hệ thống bằng các ngôn ngữ UML[1], OCL[5], Alloy[2] và một phương pháp để kiểm tra các yếu tố mô hình. Trong đó nắm rõ cách thức chuyển đổi biểu đồ lớp UML[1] sang mô hình Alloy[2]. Trong điều kiện xây dựng hoàn chỉnh cơ sở lý thuyết chuyển đổi từ đặc tả biểu đồ lớp UML[1] sang Alloy[2], chúng ta có thể xây dựng công cụ tự động chuyển biểu đồ lớp UML[1] sang Alloy[2]. Alloy[2] cũng hỗ trợ kiểm tra mối quan hệ làm mịn giữa các đặc tả Alloy[2]. Khả năng này của Alloy[2] có thể được sử dụng để kiểm tra mối quan hệ làm mịn giữa 2 đặc tả UML[1]. Tuy nhiên vì thời gian và khả năng có hạn, em chưa thực hiện được ví dụ minh họa cho khả năng này. Em sẽ thực hiện nó trong thời gian tới cùng với việc hoàn thiện các quy tắc chuyển đổi từ mô hình UML[1] sang mô hình Alloy[2] với các trường hợp phức tạp. 43 TÀI LIỆU THAM KHẢO Tài liệu tham khảo tiếng Việt [1]TS. Dương Kiều Hoa – Tôn Thất An – Phân tích và thiết kế hệ thống thông tin theo UML Tài liệu tham khảo tiếng Anh [2] Daniel Jackson – Software Abstractions: Logic, Language, and Analysis – The Mit Press Cambridge, Massachussets London England, 2006 [3]Martin Gogolla, Mark Richters – Expressing UML Class Diagrams Properties with OCL – University of Bremen, FB 3, Computer Science Department , Germany. [4]Kyriakos Anastasakis – UML2Alloy Reference manual – The University of Birmingham School of Computer Science. [5]Object Management Group – Object Constraint Language Version 2.2 [6] [7] [8]Deitel – How to program C++ sixth edition chapter 13