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

Nội dung text: Giáo trình Đặc tả hình thức - Chương 6: Các module trong Alloy - Nguyễn Thị Minh Tuyền

1. LOGO Đặc tả hình thức Các module trong Alloy Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1
2. 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 Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
3. 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] } Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
4. 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] } Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức
5. 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 Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
6. Đị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. Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
7. Đị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 đủ. Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
8. Ví dụ module C/F/mod A B open D/lib1 open C/E/H/lib2 C D open C/E/G/lib3 lib1 E F modulePathName trong module header chỉ đặc G mod H tả đường dẫn gốc cho mọi file được import lib3 lib2 Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
9. Đị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/ family.als lib people.als Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
10. Đị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/ lib myProject people.als family.als Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
11. 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. Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
12. 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 Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
13. 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] } Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức
14. 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. Nguyễn Thị Minh Tuyền 14 Đặc tả hình thức
15. 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] } Nguyễn Thị Minh Tuyền 15 Đặc tả hình thức
16. 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ử đó. Nguyễn Thị Minh Tuyền 16 Đặc tả hình thức
17. 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 } Nguyễn Thị Minh Tuyền 17 Đặc tả hình thức
18. 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 Nguyễn Thị Minh Tuyền 18 Đặc tả hình thức
19. 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)) } Nguyễn Thị Minh Tuyền 19 Đặc tả hình thức
20. 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) } Nguyễn Thị Minh Tuyền 20 Đặc tả hình thức
21. 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] } Nguyễn Thị Minh Tuyền 21 Đặc tả hình thức
22. 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) } Nguyễn Thị Minh Tuyền 22 Đặc tả hình thức