Bài giảng Nhập môn công nghệ phần mềm: Chương 5 - Nguyễn Thanh Bình

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

Thêm vào BST

Báo xấu

15
lượt xem 2
download

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

Bài giảng "Nhập môn công nghệ phần mềm - Chương 5: Đặc tả Z" cung cấp cho người đọc các kiến thức: Giới thiệu, kiểu dữ liệu, vị từ, sơ đồ trạng thái, sơ đồ thao tác, toán tử sơ đồ, quan hệ, partial function,... Mời các bạn cùng tham khảo.

Chủ đề:

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

Lưu

Nội dung Text: Bài giảng Nhập môn công nghệ phần mềm: Chương 5 - Nguyễn Thanh Bình

ðặc tả Z (5) Nguyễn Thanh Bình Khoa Công nghệ Thông tin Trường ðại học Bách khoa ðại học ðà Nẵng Giới thiệu ñược ñề xuất bởi Jean René Abrial ở ðại học Oxford ngôn ngữ ñặc tả hình thức ñược sử dụng rộng rãi nhất dựa trên lý thuyết tập hợp ký hiệu toán học sử dụng các sơ ñồ (schema) dễ hiểu 2 1 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Giới thiệu Gồm bốn thành phần cơ bản các kiểu dữ liệu (types) • dựa trên khái niệm tập hợp các sơ ñồ trạng thái (state schemas) • mô tả các biến và ràng buộc trên các biến các sơ ñồ thao tác (operation schemas) • mô tả các thao tác (thay ñổi trạng thái) các toán tử sơ ñồ (schema operations) • ñịnh nghĩa các sơ ñồ mới từ các sơ ñồ ñã có 3 Kiểu dữ liệu mỗi kiểu dữ liệu là một tập hợp các phần tử Ví dụ {true, false} : kiểu lô-gíc N: kiểu số tự nhiên Z: kiểu số nguyên R: kiểu số thực {red, blue, green} 4 2 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Kiểu dữ liệu Các phép toán trên tập hợp Hội: A∪B Giao: A∩B Hiệu: A⁄B Tập con: A⊆B Tập các tập con: P A • ví dụ: P {a, b} = {{}, {a}, {b}, {a, b}} 5 Kiểu dữ liệu 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 ... có thể ñịnh nghĩa các kiểu dữ liệu mới ANSWER == yes | no [PERSON] • sử dụng cặp ký hiệu [ và ] ñể ñịnh nghĩa kiểu cơ bản mới 6 3 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Kiểu dữ liệu Khai báo kiểu x:T • x là phần tử của tập T Ví dụ • x:R • n:N • 3:N • red : {red, blue, green} 7 Vị từ Một vị từ (predicate) ñược sử dụng ñể ñịnh nghĩa các tính chất của biến/giá trị Ví dụ x>0 π∈R 8 4 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Vị từ Có thể sử dụng các toán tử lô-gíc ñể ñịnh nghĩa các vị từ phức tạp Và: A∧B Hoặc: A∨B Phủ ñịnh: ¬A Kéo theo: A⇒B Ví dụ (x > y) ∧ (y > 0) (x > 10) ∨ (x = 1) (x > 0) ) ⇒ x/x = 1 (¬ (x ∈ S)) ∨ (x ∈ T) 9 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} 10 5 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Sơ ñồ trạng thái Cấu trúc sơ ñồ trạng thái gồm tên sơ ñồ khai báo biến ñịnh nghĩa vị từ 11 Sơ ñồ trạng thái ðặc tả Z chứa các biến trạng thái khởi gán biến các thao tác trên các biến biến trạng thái có thể có các bất biến • ñiều kiện mà luôn ñúng, biểu diễn bởi các vị từ 12 6 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Sơ ñồ thao tác Khởi gán biến Khai báo thao tác trên biến kí hiệu ∆ biểu diễn biến trạng thái bị thay ñổi bởi thao tác kí hiệu ‘ (dấu nháy ñơn) biểu diễn giá trị mới của biến 13 Sơ ñồ thao tác Thao tác có thể có các tham số vào và ra tên tham số vào kết thúc bởi kí tự “?” tên tham số ra kết thúc bởi kí tự “!” 14 7 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Sơ ñồ thao tác Kí hiệu Ξ mô tả thao tác không thể thay ñổi biến trạng thái 15 Ví dụ 1 ðặc tả hệ thống ghi nhận các nhân viên vào/ra tòa nhà làm việc Kiểu dữ liệu [Staff] là kiểu cơ bản mới của hệ thống Trạng thái của hệ thống bao gồm • tập hợp các người sử dụng hệ thống user • tập hợp các nhân viên ñang vào in • tập hợp các nhân viên ñang ra out bất biến của hệ thống 16 8 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Ví dụ 1 ðặc tả thao tác ghi nhận một nhân viên vào 17 Ví dụ 1 ðặc tả thao tác ghi nhận một nhân viên ra 18 9 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Ví dụ 1 ðặc tả thao tác kiểm tra một nhân viên vào hay ra Thao tác này cho kết quả là phần tử của kiểu QueryReply == is_in | is_out ðặc tả thao tác 19 Ví dụ 1 Khởi tạo hệ thống 20 10 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Ví dụ 1 Tóm lại Sơ ñồ trạng thái: các thành phần/ñối tượng của hệ thống Bất biến: ràng buộc giữa các ñối tượng Các sơ ñồ thao tác • ðiều kiện trên các tham số vào • Quan hệ giữa trạng thái trước và sau • Tham số kết quả Khởi gán 21 Ví dụ 1 Hãy ñặc tả các thao tác Register: thêm vào một nhân viên mới QueryIn: cho biết những nhân viên ñang vào/làm việc 22 11 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Toán tử sơ ñồ Các sơ ñồ có thể ñược kết hợp ñể tạo ra các sơ ñồ mới Các toán tử sơ ñồ Và: ∧ Hoặc: ∨ 23 Toán tử sơ ñồ Các sơ ñồ ñã có Tạo các sơ ñồ mới Schema3 == Schema1 ∧ Schema2 Schema4 == Schema1 ∨ Schema2 24 12 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Ví dụ 1 (tiếp) Cải tiến thao tác StaffQuery Thao tác StaffQuery chưa ñặc tả trường hợp lỗi • name? ∉ users 25 Ví dụ 1 (tiếp) Cải tiến thao tác StaffQuery ðặc tả lại kiểu QueryReply QueryReply == is_in | is_out | not_registered Khi ñó RobustStaffQuery == StaffQuery ∨ BadStaffQuery 26 13 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Ví dụ 1 (tiếp) Cải tiến thao tác CheckIn Mở rộng thao tác cho trường hợp ghi nhận thành công 27 Ví dụ 1 (tiếp) Cải tiến thao tác CheckIn Mở rộng thao tác cho trường hợp ghi nhận thành công Khi ñó GoodCheckIn == CheckIn ∧ Success 28 14 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Ví dụ 1 (tiếp) Cải tiến thao tác CheckIn Xử lý thêm hai trường hợp lỗi 1. name? ñã ñược ghi nhận 2. name? chưa ñược ñăng ký 29 Ví dụ 1 (tiếp) Cải tiến thao tác CheckIn Xử lý thêm hai trường hợp lỗi 30 15 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Ví dụ 1 (tiếp) Cải tiến thao tác CheckIn Khi ñó CheckInReply == ok | already_in | not_registered RobustCheckIn == GoodCheckIn ∨ BadCheckIn1 ∨ BadCheckIn2 31 Quan hệ Cặp phần tử có thứ tự ñược biểu diễn (x, y) Tích ðề-các của hai kiểu T1 và T2 T1 x T2 (x, y) : T1 x T2 32 16 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Quan hệ Quan hệ (relation) là tập các cặp phần tử có thứ tự Ví dụ: 33 Quan hệ Có thể ký hiệu quan hệ T ↔ S == P (T x S) directory : Person ↔ Number Ánh xạ cặp phần tử có thứ tự (x, y) có thể viết • Ví dụ Lưu ý kí hiệu ↔ dành cho kiểu kí hiệu dành cho giá trị 34 17 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Quan hệ Domain và Range tập hợp các thành phần thứ nhất trong một quan hệ ñược gọi là domain (miền) • kí hiệu: dom • ví dụ: dom(directory) = {mary, john, jim, jane} tập hợp các thành phần thứ hai trong một quan hệ ñược gọi là range • kí hiệu: ran • ví dụ: ran(directory) = {287373, 398620, 829483, 493028} 35 Quan hệ Phép trừ miền (domain subtraction) ký hiệu: biểu diễn quan hệ R với các phần tử trong miền S ñã bị loại bỏ Nghĩa là: 36 18 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Quan hệ Phép trừ miền (domain subtraction) Ví dụ: Khi ñó: 37 Ví dụ 2 ðặc tả danh bạ ñiện thoại gồm tên người và số ñiện thoại Sử dụng kiểu cơ bản [Person, Phone] ðặc tả trạng thái hệ thống 38 19 CuuDuongThanCong.com https://fb.com/tailieudientucntt
Ví dụ 2 Khởi tạo hệ thống Thêm một số ñiện thoại 39 Ví dụ 2 có thể cải tiến ? Tìm số ñiện thoại của một người Tìm tên theo số ñiện thoại 40 20 CuuDuongThanCong.com https://fb.com/tailieudientucntt