Bài giảng Đặc tả hình thức: Chương 5 - PGS.TS. Vũ Thanh Nguyên

Bài giảng Đặc tả hình thức: Chương 5 Đặc tả hàm, cung cấp cho người đọc những kiến thức như: Tổng quan về hàm; Đặc tả hàm không tường minh; Đặc tả hàm tường minh; Đặc tả đệ quy và sử dụng hàm phụ; Một số cấu trúc điều khiển. 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 Đặc tả hình thức: Chương 5 - PGS.TS. Vũ Thanh Nguyên Trường Đại học Công Nghệ Thông Tin, ĐHQG-HCM Khoa Công Nghệ Phần Mềm Chương 5: Đặc tả hàm TS. Vũ Thanh Nguyên 23-02-2023 TS. Vũ Thanh Nguyên 1 Nội dung  Tổng quan về hàm  Đặc tả hàm không tường minh  Đặc tả hàm tường minh  Đặc tả đệ quy và sử dụng hàm phụ  Một số cấu trúc điều khiển 23-02-2023 TS. Vũ Thanh Nguyên 2 Tổng Quan Về Hàm  Hàm là một khái niệm trừu tượng toán học: là ánh xạ giữa hai tập giá trị.  function_name: domain → range, ở đó function_name: tên của hàm domain: miền xác định của tập giá trị mà ở đó hàm có thể ứng dụng range: phạm vi xác định của tập giá trị mà ở đó hàm chứa đựng kết quả của ứng dụng hàm. giữa domain và range cách nhau bằng →  Nếu miền xác định có từ 2 giá trị trở lên, cần dùng dấu gcd: N1xN1 → N1 23-02-2023 TS. Vũ Thanh Nguyên 3 Tổng Quan Về Hàm  Định nghĩa hàm. Hàm có thể được định nghĩa nhờ vào các phép toán và hằng số  Ví dụ: Hàm định nghĩa trực tiếp (tường minh) của bình phương square: Z → N square(i) ≜ i*i Hàm xác định giá trị tuyệt đối abs: Z → N abs(i) ≜ if i Tổng Quan Về Hàm  Hàm chia hết divides: N1N → B divides(i,j) ≜ j mod i = 0 Sử dụng toán tử dạng infix  i divides j Hàm xác định số chẵn is-even: N → B is-even(i) ≜ 2 divides i Hàm xác định số lẻ is-odd: N → B is-odd(i) ≜ ¬is-even(i) 23-02-2023 TS. Vũ Thanh Nguyên 5 Tổng Quan Về Hàm  Hàm ước số chung của 2 số is-common-divisor: NNN1 → B is-common-divisor(i,j,d) ≜ d divides i  d divides j Hàm xác định giá trị nhỏ hơn 3 less-than-three: N → B less-than-three(i) ≜ i Tổng Quan Về Hàm  Hàm xác định số nguyên tố is-prime: N → B is-prime(i) ≜ i1  dN1  d divides i  d=1  d=i hoặc có thể định nghĩa is-prime(i) ≜ i1  d{2,…,i-1}  ¬(d divides i) 23-02-2023 TS. Vũ Thanh Nguyên 7 Các phép tổng quát trên ngôn ngữ VDM 23-02-2023 TS. Vũ Thanh Nguyên 8 Đặc tả hàm  Ví dụ:  Hàm luỹ thừa có thể được xác định bằng phương pháp tường minh bằng hàm exponent_x như sau: exponent_x: ZN→Z exponent_x(x,n) ≜ if n=0 then 1 else xexponent_x(x,n-1) 23-02-2023 TS. Vũ Thanh Nguyên 9 Đặc tả hàm  Ví dụ:  Hàm luỹ thừa củng có thể được xác định bằng phương pháp không tường minh như sau: EXPONENT(x:Z, n:N)y:Z pre true post y=xn 23-02-2023 TS. Vũ Thanh Nguyên 10 Đặc tả hàm không tường minh  Đặc tả hàm không tường minh (implicit definition):  Phát biểu trạng thái hệ thống trước và sau khi thực hiện hàm  Không cần nêu ra các bước để thực hiện xử lý trong hàm tên_hàm (thamsố1: Kiểu1, thamsố2: Kiểu2…) kq: Kiểukq pre Vị từ pre-condition post Vị từ post-condition 23-02-2023 TS. Vũ Thanh Nguyên 11 Đặc tả hàm không tường minh  Định nghĩa tên hàm, tên và kiểu của các tham số đầu vào, tên và kiểu của kết quả trả về (tham số đầu ra)  Vị từ Pre-condition và Post-condition là biểu thức điều kiện logic, có thể có giá trị là true hoặc false.  Biểu thức điều kiện có thể chứa một hoặc nhiều vị từ. Các từ được liên kết bởi các phép liên kết logic, lượng từ và có thể chứa đựng hàm, tham số, hằng số và biến  Xác định Vị từ Pre-condition để phát biểu điều kiện về giá trị của các tham số đầu vào  Xác định Vị từ Post-condition để phát biểu mối quan hệ giữa các tham số đầu vào với kết quả trả về của hàm 23-02-2023 TS. Vũ Thanh Nguyên 12 Đặc tả hàm không tường minh  Các phép liên kết logic của vị từ Pre-condition và Post- condition   - và   - hoặc   - nếu và chỉ nếu (if and only if)   - kéo theo   - với mọi   - tồn tại  ¬ - nó không phải là trường hợp 23-02-2023 TS. Vũ Thanh Nguyên 13 Đặc tả hàm không tường minh  Theo cấu trúc chuẩn của đặc tả hàm không tường minh:  Mỗi hàm có tối đa 1 kết quả trả về  Các tham số đầu vào đều là dạng read-only (tham trị)  Vấn đề: Làm cách nào đặc tả hàm cần trả về nhiều nội dung thông tin?  Giải pháp: Định nghĩa kiểu cấu trúc để chứa tất cả các thành phần thông tin sẽ trả về (Chương 6)  Giải pháp khác??? 23-02-2023 TS. Vũ Thanh Nguyên 14 Đặc tả hàm không tường minh  Hàm được gọi là không tường minh vì vị từ post-condition không có sự giải thích cách thực hiện thuật toán  không thể tự động tính được giá trị đầu ra từ vị từ post-condition đối với các giá trị đầu vào được cho. 23-02-2023 TS. Vũ Thanh Nguyên 15 Đặc tả hàm không tường minh  Các ưu điểm của đặc tả hàm không tường minh  Sự miêu tả trực tiếp các tính chất mà người sử dụng quan tâm  Mô tả một tập các kết quả có thể bởi vị từ post-condition  Giá trị tường minh (giá trị true hoặc false) của vị từ pre- condition  Ít xem xét tới đặc tả thuật toán  Dự kiến cho tên của kết quả 23-02-2023 TS. Vũ Thanh Nguyên 16 Đặc tả hàm không tường minh  Ví dụ: max_of_set (s: ℕ-set) r: ℕ pre s  {} post (r  s)  (n  s  n  r)  Ví dụ: abs (z: ℤ) r: ℕ pre tru ...