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

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