Bài thuyết trình: Ngôn ngữ đặc tả Z

Chia sẻ: Fjff Jhghh | Ngày: | Loại File: PDF | Số trang:28

Thêm vào BST

Báo xấu

170
lượt xem 27
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

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. Nhằm giúp các bạn hiểu hơn về vấn đề này, mời các bạn cùng tham khảo nội dung bài thuyết trình "Ngôn ngữ đặc tả Z". Hy vọng đây là tài liệu tham khảo hữu ích cho các bạn.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Bài thuyết trình: 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 1 GIỚI THIỆU 2 TẬP HỢP VÀ LOGIC 3 SƠ ĐỒ 4 QUAN HỆ 55 FUNCTION
GIỚI THIỆU NGÔN NGỮ Z  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 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: