Đặc tả hình thức - Giới thiệu về Alloy (P3) - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền Giới thiệu về Alloy Nguyễn Thị Minh Tuyền 1 Đặc tả hình thức 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 } 2 Nguyễn Thị Minh Tuyền Đặ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) } 3 Nguyễn Thị Minh Tuyền Đặ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. 4 Nguyễn Thị Minh Tuyền Đặ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 5 Nguyễn Thị Minh Tuyền Đặ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 6 Nguyễn Thị Minh Tuyền Đặ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. 7 Nguyễn Thị Minh Tuyền Đặ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? 8 Nguyễn Thị Minh Tuyền Đặ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. 9 Nguyễn Thị Minh Tuyền Đặ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) 10 Nguyễn Thị Minh Tuyền Đặ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} 11 Nguyễn Thị Minh Tuyền Đặ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? 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức Trở lại ví dụ granpa 13 Nguyễn Thị Minh Tuyền 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 LOGO