Chương V: Đặc tả với ngôn ngữ Z

Ký pháp Z, hay còn được gọi là ngôn ngữ Z được xây dựng dựa trên lý thuyết tậphợp và logic toán học. Đây là một ngôn ngữ toán học chặt chẽ, được sử dụng chủyếu trong đặc tả hình thức để đặc tả các yêu cầu chức năng của 1 hệ thống, đặc biệtlà hệ thống phần mềm.Ngôn ngữ Z không được thiết kế để mô tả các yêu cầu phi chức năng của hệ thống,ví dụ như công dụng, hiệu năng, kích thước hay độ tin cậy của hệ thống. Ngôn ngữcũng không được thiết kế cho các...
Nội dung trích xuất từ tài liệu:
Chương V: Đặc tả với ngôn ngữ ZChương V: Đặc tả với ngôn ngữ Z Bài giảng môn Đặc tả Hình thức CHƯƠNG V: NGÔN NGỮ ĐẶC TẢ ZCác nội dung chính của chương:CHƯƠNG V: NGÔN NGỮ ĐẶC TẢ Z...................................................................................1 V.1 Giới thiệu .......................................................................................................................3 V.2 Các thành phần của ngôn ngữ........................................................................................3 V.2.1 Logic toán học........................................................................................................3 V.2.1.1 Logic mệnh đề..................................................................................................3 V.2.1.2 Logic vị từ.........................................................................................................3 V.2.2 Lý thuyết tập hợp..................................................................................................5 V.2.3 Hàm và quan hệ.....................................................................................................6 V.2.3.1 Quan hệ 2 ngôi..................................................................................................6 V.2.3.2 Miền xác định và miền giá trị..........................................................................6 V.2.3.3 Hàm...................................................................................................................6 V.2.3.4 Hàm riêng phần.................................................................................................6 V.2.3.5 Hàm toàn phần..................................................................................................6 V.3 Giản đồ (schemas)..........................................................................................................7 V.3.1 Giới thiệu chung....................................................................................................7 V.3.2 Định nghĩa..............................................................................................................7 V.3.3 Toán tử đặt tên.......................................................................................................8 V.3.4 Giản đồ tương đương...........................................................................................8 V.3.5 Một số ghi chú ......................................................................................................8 V.3.6 Giản đồ được sử dụng như 1 kiểu dữ liệu.........................................................9 V.3.7 Giản đồ được sử dụng trong các khai báo.........................................................10 V.3.8 Giản đồ được sử dụng trong các biểu thức lượng từ.......................................11 V.3.9 Giản đồ được sử dụng như 1 vị từ....................................................................11 V.3.10 Dạng chuẩn của 1 giản đồ...............................................................................12 V.3.11 Đặt lại tên các thành phần trong giản đồ.........................................................13 V.4 Các phép toán trên giản đồ...........................................................................................13 V.4.1 Phép nối liền (Conjunction).................................................................................13 V.4.2 Phép đổi tên (Decoration)....................................................................................14 V.4.3 Phép nối rời (Disjunction)...................................................................................15 V.4.4 Phép phủ định (Negation)....................................................................................15Biên soạn: Nguyễn Trần Thi Văn 1Chương V: Đặc tả với ngôn ngữ Z Bài giảng môn Đặc tả Hình thức V.4.5 Phép lượng từ hóa ...............................................................................................16 V.5 Bài tập áp dụng.............................................................................................................17Biên soạn: Nguyễn Trần Thi Văn 2Chương V: Đặc tả với ngôn ngữ Z Bài giảng môn Đặc tả Hình thứcV.1 Giới thiệu Ký pháp Z, hay còn được gọi là ngôn ngữ Z được xây dựng dựa trên lý thuyết tập hợp và logic toán học. Đây là một ngôn ngữ toán học chặt chẽ, được sử dụng chủ yếu trong đặc tả hình thức để đặc tả các yêu cầu chức năng của 1 hệ thống ...