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

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.
Nội dung trích xuất từ tài liệu:
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 ...