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

LOGO<br /> <br /> Đặc tả hình thức<br /> Giới thiệu về Alloy<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 1<br /> <br /> Các phép toán logic<br /> v Những phép toán<br /> not<br /> !<br /> and<br /> &&<br /> or<br /> ||<br /> implies<br /> =><br /> else<br /> <br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> logic thường dùng<br /> negation<br /> conjunction<br /> disjunction<br /> implication<br /> alternative<br /> iff<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Thứ tự ưu tiên các phép toán<br /> ||<br /> <br /> =><br /> &&<br /> !<br /> = != in<br /> + ++<br /> &<br /> -><br /> <br /> []<br /> .<br /> ~ * ^<br /> Nguyễn Thị Minh Tuyền<br /> <br /> thấp<br /> <br /> cao<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> Ví dụ<br /> v Giả sử một sổ địa chỉ được mô hình hóa:<br /> §  homeAddress và workAddress ánh xạ một bí danh (alias) tới địa<br /> chỉ email cá nhân và dùng cho công việc, và địa chỉ ánh xạ một bí<br /> danh tới một địa chỉ thường dùng.<br /> §  Để nói rằng địa chỉ thường dùng cho một bí danh a nào đó là địa<br /> chỉ email sử dụng cho công việc nếu nó tồn tại, nếu không đó sẽ<br /> là địa chỉ email cá nhân, ta có thể viết:<br /> some a.workAddress =><br /> a.address = a.workAddress<br /> else a.address = a.homeAddress<br /> hoặc sử dụng các biểu thức điều kiện<br /> a.address =<br /> some a.workAddress => a.workAddress<br /> else a.homeAddress<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> v  a!=b tương đương với not a = b<br /> có thể viết a not = b<br /> v  Từ khóa else có thể được dùng với toán tử implies<br /> §  F implies G else H<br /> §  tương đương với (F and G) or (not F) and H<br /> <br /> v  Toán từ implies có thể lồng nhau<br /> § <br /> § <br /> § <br /> § <br /> <br /> C1 implies F1<br /> else C2 implies F2<br /> else C3 implies F3<br /> với điều kiện C1 thì F1 đúng, nếu không với điều kiện C2 thì F2 đúng,<br /> nếu không với điều kiện C3 thì F3 đúng.<br /> <br /> v {F G H} tương đương F and G and H<br /> v C implies E1 else E2 có thể viết C => E1 else<br /> E2.<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />