Bài giảng Đặc tả hình thức - Chương 6: Các module trong Alloy - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền Các module trong Alloy Nguyễn Thị Minh Tuyền 1 Đặc tả hình thức Module trong Alloy v Alloy là một hệ thống module cho phép module hóa việc sử dụng lại các mô hình. v Một module định nghĩa một mô hình và có thể xem mô hình này là một mô hình con của mô hình khác. v Để thuận lợi cho việc tái sử dụng, các module có thể được tham số hóa trong một hoặc nhiều signature 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ module util/relation -- r is acyclic over the set s pred acyclic [r: univ->univ, s: set univ] { all x: s | x !in x.^r } module family open util/relation as rel sig Person { parents: set Person } fact { acyclic [parents, Person] } 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ module util/relation -- r is acyclic over the set s pred acyclic [r: univ->univ, s: set univ] { all x: s | x !in x.^r } module fileSystem open util/relation as rel sig Object {} sig Folder extends Object { subFolders: set Folder } fact { acyclic [subFolders, Folder] } 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Khai báo module v Dòng đầu tiên của mỗi module là module header module modulePathName v Module có thể import một module khác với câu lệnh open ngay sau header open modulePathName 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức Định nghĩa module v Một module A có thể import một module B, module B lại có thể import một module C ... v Không cho phép có bất cứ vòng lặp nào trong cấu trúc import. 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức Định nghĩa ModulePathName v Mỗi module có một tên đường dẫn, tên này phải khớp với đường dẫn của file chứa module đó trong hệ thống file. v Tên đường dẫn module có thể §  chỉ là tên file (mà không có phần mở rộng .als) §  có thể là đường dẫn đầy đủ. 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ module C/F/mod open D/lib1 open C/E/H/lib2 open C/E/G/lib3 modulePathName trong module header chỉ đặc tả đường dẫn gốc cho mọi file được import 8 Nguyễn Thị Minh Tuyền A B C D E F G H lib1 mod lib2 lib3 Đặc tả hình thức Định nghĩa ModulePathName v Ví dụ: module family open lib/people v Nếu đường dẫn của family.als là trong hệ thống file thì AA sẽ tìm kiếm people.als trong /lib/ 9 Nguyễn Thị Minh Tuyền family.als people.als lib Đặc tả hình thức Định nghĩa ModulePathName v Ví dụ: module myProject/family open lib/people v Nếu đường dẫn của myProject là trong hệ thống file thì AA sẽ tìm kiếm people.als trong /lib/ 10 Nguyễn Thị Minh Tuyền family.als people.als lib myProject Đặc tả hình thức Các module định nghĩa sẵn v Alloy 4 có một thư viện các module được định nghĩa sẵn. v Bất kỳ một module nào được import thì AA sẽ tìm kiếm trong các module này đầu tiên. 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức As v Khi tên đường dẫn của một import chứa / (ví dụ như đó không chỉ là tên file mà còn là đường dẫn) v Thì ta phải đưa ra một tên ngắn hơn cho module với từ khóa as. open util/relation as rel 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức Xung đột về tên v Các module có không gian tên (namespace) riêng. v Để tránh xung đột tên giữa các thành phần của các module khác nhau, ta dùng qualified name. module family open util/relation as rel sig Person { parents: set Person } fact { rel/acyclic [parents] } 13 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các module được tham số hóa v Một mô hình m có thể được tham số hóa bởi một hoặc nhiều tham số signature [x1,...,xn] v Hiệu ứng của việc mở m[s1,...,sn] là import một bản copy của m với mỗi tham số của signature xi được thay thế bởi tên signature si. 14 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ module graph [node] // 1 signature param open util/relation as rel pred dag [r: node -> node] { acyclic [r, node] } module family open util/graph [Person] as g sig Person { parents: set Person } fact { dag [parents] } 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức Module định nghĩa sẵn: Ordering v Tạo ra một chuỗi có thứ tự các nguyên tử trong module S: module util/ordering[S] v Nếu scope trên một signature là 5 thì opening ordering[S] sẽ buộc S phải có 5 phần tử và tạo ra một chuỗi tuyến tính trên 5 phần tử đó. 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức Module Ordering module util/ordering[S] private one sig Ord { First, Last: S, Next, Prev: S -> lone S } fact { // all elements of S are totally ordered S in Ord.First.*Next ... } 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức Module Ordering // constraints that actually define the // total order Ord.Prev = ~(Ord.Next) one Ord.First one Ord.Last no Ord.First.Prev no Ord.Last.Next 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức Module Ordering { // either S has exactly one atom, // which has no predecessors or successors ... (one S and no S.(Ord.Prev) and no S.(Ord.Next)) or // or ... all e: S | // ... each element except the first has one predecessor, and ... (e = Ord.First or one e.(Ord.Prev)) and // ...each element except the last has one successor, and ... (e = Ord.Last or one e.(Ord.Next)) and // ... there are no cycles (e !in e.^(Ord.Next)) } 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức Module Ordering // first fun first: one S { Ord.First } // last fun last: one S { Ord.Last } // return the predecessor of e, or empty set if e is //the first element fun prev [e: S]: lone S{ e.(Ord.Prev) } // return the successor of e, or empty set of e is // the last element fun next [e: S]: lone S { e.(Ord.Next) } // return elements prior to e in the ordering fun prevs [e: S]: set S { e.^(Ord.Prev) } // return elements following e in the ordering fun nexts [e: S]: set S { e.^(Ord.Next) } 20 Nguyễn Thị Minh Tuyền Đặc tả hình thức Module Ordering // e1 is before e2 in the ordering pred lt [e1, e2: S] { e1 in prevs[e2] } // e1 is after than e2 in the ordering pred gt [e1, e2: S] { e1 in nexts[e2] } // e1 is before or equal to e2 in the ordering pred lte [e1, e2: S] { e1=e2 || lt [e1,e2] } // e1 is after or equal to e2 in the ordering pred gte [e1, e2: S] { e1=e2 || gt [e1,e2] } 21 Nguyễn Thị Minh Tuyền Đặc tả hình thức Module Ordering // returns the larger of the two elements in the ordering fun larger [e1, e2: S]: S { lt[e1,e2] => e2 else e1 } // returns the smaller of the two elements in the ordering fun smaller [e1, e2: S]: S { lt[e1,e2] => e1 else e2 } // returns the largest element in es // or the empty set if es is empty fun max [es: set S]: lone S { es - es.^(Ord.Prev) } // returns the smallest element in es // or the empty set if es is empty fun min [es: set S]: lone S { es - es.^(Ord.Next) } 22 Nguyễn Thị Minh Tuyền LOGO