intTypePromotion=1
zunia.vn Tuyển sinh 2024 dành cho Gen-Z zunia.vn zunia.vn
ADSENSE
 » 
 » 

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

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

Thêm vào BST
Báo xấu
5
lượt xem 3
download
 
  Download Vui lòng tải xuống để xem tài liệu đầy đủ

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!

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 Đặc tả hình thức: Chương 5 - PGS.TS. Vũ Thanh Nguyên

  1. 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
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. Các phép tổng quát trên ngôn ngữ VDM 23-02-2023 TS. Vũ Thanh Nguyên 8
  9. Đặ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
  10. Đặ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
  11. Đặ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
  12. Đặ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
  13. Đặ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
  14. Đặ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
  15. Đặ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
  16. Đặ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
  17. Đặ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 true post ((r = z)  (z  0))  ((r = -z)  (z < 0)) 23-02-2023 TS. Vũ Thanh Nguyên 17
  18. Đặc tả hàm không tường minh  Ví dụ: hàm tính ước số chung lớn nhất bằng phương pháp không tường minh sử dụng lượng từ như sau:  gcd (i:N1, j:N1) r:N1 pre true post is-common-divisor (i,j,r)  ¬ sN1  is-common-divisor (i,j,s)  s>r 23-02-2023 TS. Vũ Thanh Nguyên 18
  19. Đặc tả hàm không tường minh  Ví dụ: tính căn bật hai của một số nguyên int_sqr (x: ℕ) z:ℕ pre x≥1 post (z2 ≤ x)  (x < (z+1)2)  Ví dụ: hàm trả lại số dư của số nguyên y chia cho số nguyên x mod (x,y:N)m:ℕ pre (x > 0)  (y > 0) post dZ (y=dx+m)  (0≤m)  (m
  20. Đặc tả hàm không tường minh  Ví dụ: Hàm trả về vị trí xuất hiện đầu tiên của chuỗi pt trong chuỗi cx, hoặc trả về 0 nếu chuỗi pt không xuất hiện trong cx ?  Thảo luận:? 23-02-2023 TS. Vũ Thanh Nguyên 20
ADSENSE

CÓ THỂ BẠN MUỐN DOWNLOAD

THÔNG TIN
TRỢ GIÚP
HỖ TRỢ KHÁCH HÀNG
Theo dõi chúng tôi

Chịu trách nhiệm nội dung:

Nguyễn Công Hà - Giám đốc Công ty TNHH TÀI LIỆU TRỰC TUYẾN VI NA

LIÊN HỆ

Địa chỉ: P402, 54A Nơ Trang Long, Phường 14, Q.Bình Thạnh, TP.HCM

Hotline: 093 303 0098

Email: support@tailieu.vn

Giấy phép Mạng Xã Hội số: 670/GP-BTTTT cấp ngày 30/11/2015 Copyright © 2022-2032 TaiLieu.VN. All rights reserved.

 

Đồng bộ tài khoản
3=>0