Ngôn ngữ đặc tả z

NGÔN NGỮ ĐẶC TẢ Z NHÓM 06:  TRẦN XUÂN THỊNH LÊ TRỌNG LINH LÊ MINH TRIỂN PHAN VĂN THẠCH NGUYỄN ANH ĐỨC NGÔN NGỮ ĐẶC TẢ Z GIỚI THIỆU 1 TẬP HỢP VÀ LOGIC 2 SƠ ĐỒ 3 QUAN HỆ 4 FUNCTION 5 5  Ngôn ngữ Z là ngôn ngữ đặc tả hình thức cho hệ thống máy tính dựa trên cơ sở lý thuyết tập hợp, logic vị từ và sử dụng sơ đồ để biểu diễn.  Ngôn ngữ đặc tả hình thức sử dụng các ký hiệu toán học để mô tả chính xác các thuộc tính mà không phụ thuộc vào cách thuộc tính đó được thực hiện.  Chúng mô tả những gì hệ thống phải làm chứ không không nói rõ chúng được thực hiện như thế nào. GIỚI THIỆU NGÔN NGỮ Z GIỚI THIỆU NGÔN NGỮ Z Gồm 4 thành phần cơ bản:  Các kiểu dữ liệu  Sơ đồ trạng thái  Sơ đồ thao tác  Các toán tử sơ đồ TẬP HỢP Tập hợp là các kiểu cơ bản nhất trong ngôn ngữ Z  Các ví dụ về tập hợp:  { 3, 6, 7 }  { windows, unix, mac }  { false, true }  N (the set of natural numbers)  Z (the set of integers)  R (the set of real numbers)  {} (the empty set) TẬP HỢP  Các phép toán trên tập hợp:  Union: S ∪ T  Intersection: S ∩ T  Difference: S \ T  Subset: S ⊆ T  E.g., {c, b} ⊆ {a, b, c}.  Power Set: P S (set of subsets of S).  E.g.,  P{a, b, c} = { {}, {a}, {b}, {c},{a, b}, {b, c}, {a, c},{a, b, c} } KIỂU  Kiểu được sử dụng để phân biệt các hình thức khác nhau của dữ liệu được biểu diển trong đặc tả  Một số kiểu dữ liệu cơ bản đã được định nghĩa trước  kiểu số nguyên Z  kiểu số tự nhiên N  Kiểu số thực R  ...  Định nghĩa các kiểu dữ liệu mới bằng cách đặt tên của nó giữa 2 dấu ngoặc vuông []  [ Name, Address ]  Nếu chúng ta biết chính xác các giá trị của kiểu thì chúng ta sử dụng khai báo kiểu liệt kê. Vd: Direction == north | south | east | west VỊ TỪ  Vị từ dùng để định nghĩa tính chất của biến hoặc giá trị  Ví dụ • x > 0 • π ∈ R  Có thể sử dụng các toán tử logic để định nghĩa các vị từ phức tạp  And A ∧ B  Or A ∨ B  A ⇒ B  Not ¬ A VỊ TỪ  Các toán tử khác  (∀x : T • A) • A đúng với mọi x thuộc T • Ví dụ: (∀x : N • x - x =0)  (∃x : T • A) • A đúng với một số giá trị x thuộc T • Ví dụ: (∃x : R • x + x = 4)  {x : T | A} • biểu diễn các phần tử x của T thỏa mãn A • Ví dụ: N = {x : Z | x ≥ 0} GIẢN ĐỒ  Là cú pháp của Z cho phép người đặc tả định nghĩa 1 khái niệm, 1 yếu tố mới gồm nhiều thành phần thông tin khác nhau,có ràng buộc với nhau.  1 giản đồ gồm 2 thành phần:  Phần khai báo các biến  Phần vị từ diễn tả các ràng buộc trên những biến này.  Giản đồ được biểu diễn 1 trong 2 dạng sau: GIẢN ĐỒ  Ví dụ: hay GIẢN ĐỒ Toán tử đặt tên: Nhằm mục đích đặt tên cho 1 giản đồ, tiện cho việc sử dụng lại sau này. Ngôn ngữ Z cung cấp 1 toán tử riêng, được ký hiệu là: ^=. Tên ^= [khai báo | ràng buộc].  GIẢN ĐỒ Hai giản đồ được gọi là tương đương nhau nếu: • Có cùng các biến • Cùng ràng buộc giống nhau trên các biến. GIẢN ĐỒ Dạng chuẩn của giản đồ:  Tất cả các ràng buộc đều nằm ở phần ràng buộc bên dưới.  Thao tác chuyển toàn bộ ràng buộc xuống phần dưới của giản đồ được gọi là chuẩn hóa giản đồ CÁC PHÉP TOÁN TRÊN GIẢN ĐỒ Phép nối liền: Cho 2 giản đồ S & T ; P,Q là 2 vị từ diễn tả các ràng buộc lên các biến. Phép nối liền S & T được ký hiệu S^T: CÁC PHÉP TOÁN TRÊN GIẢN ĐỒ Phép đổi tên: Giả sử ta có giản đồ State mô tả 1 trạng thái của hệ thống. Để phân biệt 2 trạng thái trước và sau khi thực hiện thao tác, ta sử dụng dấu phẩy sau tên giản đồ và các biến. CÁC PHÉP TOÁN TRÊN GIẢN ĐỒ Phép nối rời: Cho 2 giản đồ S & T ; P,Q là 2 vị từ diễn tả các ràng buộc lên các biến.  Phép nối rời S & T được ký hiệu SVT: CÁC PHÉP TOÁN TRÊN GIẢN ĐỒ Phép phủ định: Cho giản đồ S ; P là vị từ diễn tả các ràng buộc lên các biến. Chú ý: Phép phủ định chỉ được sự dụng cho các giản đồ đã được chuẩn hóa CÁC PHÉP TOÁN TRÊN GIẢN ĐỒ Phép lượng từ hóa: Nếu Q là một lượng từ và dec là phần khai báo, khi đó giản đồ được lượng từ hóa sẽ có dạng. Giản đồ nay được tạo thành bằng cách bỏ đi các thành phần có trong phần khai báo dec và lượng từ hóa chúng bằng lượng từ Q trong phần vị từ ràng buộc bên dưới. CÁC PHÉP TOÁN TRÊN GIẢN ĐỒ Phép lượng từ hóa: QUAN HỆ  Quan hệ là tập các cặp phần tử có thứ tự Numberperson  Có thể ký hiệu quan hệ + (TXS) + Directory : PST  QUAN HỆ Ánh xạ: • cặp phần tử có thứ tự (x,y) có thể viết: Lưu ý: Kí hiệu dành cho kiểu Kí hiệu dành cho giá trị yx   QUAN HỆ Domain và Range Tập hợp các thành phần thứ nhất trong 1 quan hệ được gọi là domain. Ký hiệu: dom dom(directory) = {mary, john, jim, jane} Tập hợp các thành phần thứ hai trong 1 quan hệ được gọi là range. Ký hiệu: ran  ran(directory) = {287373, 398620, 829483, 493028} Phép trừ miền (domain subtraction) Ký hiệu: QUAN HỆ FUNCTION Partial Function Là quan hệ mà mỗi phần từ trong domain cho một giá trị duy nhất trong range. Ký hiệu: FUNCTION Partial Function Toán tử quá tải hàm: Thay thế một mục vào bởi mục mới. Ký hiệu: Ví dụ: FUNCTION Total Function Định nghĩa ánh xạ từ tất cả giá trị của domain đến range. Ký hiệu: Ví dụ: www.themegallery.com