Bài giảng Đặc tả hình thức - Bài 5: Giới thiệu về Alloy - Nguyễn Thị Minh Tuyền
Bạn đang xem tài liệu "Bài giảng Đặc tả hình thức - Bài 5: Giới thiệu về Alloy - Nguyễn Thị Minh Tuyền", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên
Tài liệu đính kèm:
- bai_giang_dac_ta_hinh_thuc_bai_5_gioi_thieu_ve_alloy_nguyen.pdf
Nội dung text: Bài giảng Đặc tả hình thức - Bài 5: Giới thiệu về Alloy - Nguyễn Thị Minh Tuyền
- LOGO Đặc tả hình thức Giới thiệu về Alloy Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1
- Assertion v Assertion là ràng buộc bổ sung và được kiểm tra bởi bộ phân tích xem chúng có đúng hay không. v Nếu một assertion không đúng, bộ phân tích sẽ tạo ra một phản ví dụ. v Cú pháp: assert tên{ ràng buộc } Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
- Ví dụ v Không ai có bố mẹ mà đồng thời cũng là anh chị em. assert parentsSiblings{ all p: Person | no p.parents & p.siblings } v Anh chị em của một người là anh chị em của những người đó. assert siblingsSiblings{ all p: Person | p.siblings = p.siblings.siblings } v Không ai có cùng tổ tiên với chồng/vợ mình ( ví dụ vợ/chồng không có quan hệ huyết thống). assert sameBlood{ no p: Married | some (p.^parents & p.spouse.^parents) } Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
- Lệnh (command) và phạm vi (scope) v Để phân tích một mô hình, ta cần một lệnh và chỉ dẫn công cụ thực thi nó. § Lệnh run yêu cầu công cụ tìm kiếm một instance của một vị từ. § Lệnh check yêu cầu công cụ tìm kiếm một phản ví dụ của một assertion. § Ví dụ: • check Safe • run trans v Để chỉ rõ một phạm vi, ta có thể đưa ra một giới hạn (scope )cho mỗi signature tương ứng với một loại cơ bản. Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức
- Check v assert a {F} v check a scope Nếu mô hình có các fact M, tìm một ví dụ sao cho M && !F v check a for default v check a for default but list v check a for list Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
- Ví dụ về check v Ví dụ: Cho trước các khai báo của một hệ thống file: abstract sig Object {} sig Directory extends Object {} sig File extends Object {} sig Alias extends File {} v và một assertion A. Các lệnh sau đây là đúng cú pháp § check A for 5 Object § check A for 4 Directory, 3 File § check A for 5 Object, 3 Directory § check A for 3 Directory, 3 Alias, 5 File Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
- Ví dụ về check v Ta có thể thiết lập một phạm vi mặc định, và có thể trộn lẫn giữa phạm vi mặc định với giới hạn rõ ràng cho một loại cụ thể. v Ví dụ: § check A for 5 § Đặt một giới hạn là 5 cho tất cả các loại top-level. § check A for 5 but 3 Directory § đặt thêm một giới hạn là 3 cho Directory, và một giới hạn là 2 cho File bằng phép suy dẫn. v Có thể dùng từ khóa exactly: § check A for exactly 3 Directory, exactly 3 Alias, 5 File § Giới hạn File với nhiều nhất 5 phần tử, nhưng yêu cầu Directory và Alias có chính xác 3 phần tử cho mỗi loại. Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
- Câu hỏi v Nếu AA không tìm được một phản ví dụ cho assertion thì assertion có hợp lệ không? Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
- Run v Được dùng để yêu cầu AA sinh ra các instance của mô hình. v AA chỉ thực thi lệnh run đầu tiên trong file. v Để phân tích một mô hình, thêm lệnh run và chỉ dẫn AA thực thi nó. v Có thể cung cấp cho lệnh run một phạm vi § giới hạn kích thước các instance được xem xét. Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
- Run và vị từ v pred p[x:X, y:Y, ] {F} v run p scope v Nếu mô hình có các fact M, tìm ví dụ sao cho M && (some x:X, y:Y|F) v fun f[x:X,y:Y, ] R{E} v run f scope v Nếu mô hình có các fact M, tìm ví dụ sao cho v M && (some x:X, y:Y, ,result:R|result = E) Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
- Ví dụ về lệnh run v Lệnh run đơn giản nhất § run {} v Lệnh run có điều kiện § run {some Man && some Woman && some Married} for 2 v Một số kịch bản khác § run {some Woman && no Man} for 7 § run {some Man && some Married && no Woman} Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
- Câu hỏi v sử dụng lệnh run cho một vị từ và check cho một assertion có khác nhau không? Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
- Trở lại ví dụ granpa 1 module language/grandpa1 2 abstract sig Person { 3 father: lone Man, 4 mother: lone Woman 5 } 6 sig Man extends Person { 7 wife: lone Woman 8 } 9 sig Woman extends Person { 10 husband: lone Man 11 } 12 fact { 13 no p: Person | p in p.^(mother + father) 14 wife = ~husband 15 } 16 assert NoSelfFather { 17 no m: Man | m = m.father 18 } 19 check NoSelfFather 20 fun grandpas (p: Person): set Person { 21 p.(mother + father).father 22 } 23 pred ownGrandpa (p: Person) { 24 p in grandpas [p] 25 } 26 run ownGrandpa for 4 Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức