Bài giảng Đặc tả hình thức: Chương 6

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

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ụ

lib1

mod

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

lib3

lib2

8 Nguyễn Thị Minh Tuyền Đặ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/

family.als

lib

people.als

9 Nguyễn Thị Minh Tuyền Đặ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/

lib

myProject

people.als

family.als

10 Nguyễn Thị Minh Tuyền Đặ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

acyclic [r, node]

open util/relation as rel pred dag [r: node -> 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 Đặc tả hình thức

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

LOGO

Đặc tả hình thức

Các module trong Alloy

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

Ví dụ

module util/relation

pred acyclic [r: univ->univ, s: set univ] {

all x: s | x !in x.^r

} module family open util/relation as rel sig Person {

} fact { acyclic [parents, Person] }

Ví dụ

module util/relation

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] }

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

Đị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.

Đị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ể

Ví dụ

lib1

mod

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

lib3

lib2

Đị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/

Đị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/

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.

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

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] }

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.

Ví dụ

module graph [node] // 1 signature param

acyclic [r, node]

open util/relation as rel pred dag [r: node -> node] { }

module family

open util/graph [Person] as g sig Person { parents: set Person } fact { dag [parents] }

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ử đó.

v Alloy là một hệ thống module cho

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

v Dòng đầu tiên của mỗi module là

v Module có thể import một module khác với câu lệnh open ngay sau header

v Một module A có thể import một

v Không cho phép có bất cứ vòng lặp

v Mỗi module có một tên đường dẫn,

v Tên đường dẫn module có thể

v Ví dụ: module family

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/

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/

v Alloy 4 có một thư viện các module

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.

v Khi tên đường dẫn của một import

v Thì ta phải đưa ra một tên ngắn hơn

v Các module có không gian tên

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.

v Một mô hình m có thể được tham số

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.

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ì