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

LOGO<br /> <br /> Đặc tả hình thức<br /> Các module trong Alloy<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 1<br /> <br /> Module trong Alloy<br /> v Alloy là một hệ thống module cho<br /> phép module hóa việc sử dụng lại các<br /> mô hình.<br /> v Một module định nghĩa một mô hình<br /> và có thể xem mô hình này là một mô<br /> hình con của mô hình khác.<br /> v Để thuận lợi cho việc tái sử dụng, các<br /> module có thể được tham số hóa<br /> trong một hoặc nhiều signature<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Ví dụ<br /> module util/relation<br /> -- r is acyclic over the set s<br /> pred acyclic [r: univ->univ, s: set univ] {<br /> all x: s | x !in x.^r<br /> }<br /> module family<br /> open util/relation as rel<br /> sig Person {<br /> parents: set Person<br /> }<br /> fact { acyclic [parents, Person] }<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> Ví dụ<br /> module util/relation<br /> -- r is acyclic over the set s<br /> pred acyclic [r: univ->univ, s: set univ] {<br /> all x: s | x !in x.^r<br /> }<br /> module fileSystem<br /> open util/relation as rel<br /> sig Object {}<br /> sig Folder extends Object {<br /> subFolders: set Folder<br /> }<br /> fact { acyclic [subFolders, Folder] }<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> Khai báo module<br /> v Dòng đầu tiên của mỗi module là<br /> module header<br /> module modulePathName<br /> v Module có thể import một module<br /> khác với câu lệnh open ngay sau<br /> header<br /> open modulePathName<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />