TAILIEUCHUNG - 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! | 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

• Kỹ thuật lập trình
• Bài giảng Đặc tả hình thức
• Đặc tả hình thức
• Đặc tả hàm
• Đặc tả đệ quy
• Đặc tả hàm tường minh
• Đặc tả hàm không tường minh
• Lập trình phần mềm
• Công nghệ phần mềm
• Đặc tả phần mềm
• Ngôn ngữ đặc tả hình thức
• Đặc tả yêu cầu phần mềm
• Bài giảng Đặc tả yêu cầu phần mềm
• Công nghệ phần mềm nâng cao
• Phân loại đặc tả yêu cầu phần mềm
• Đặc tả phi hình thức phần mềm
• Đặc tả hình thức phần mềm
• Mô hình Thế giới thực
• Quy trình công nghệ phần mềm
• Ngôn ngữ hình thức
• Thiết kế ở mức cao
• Đặc tả ở mức mã nguồn
• JML nâng cao
• Từ khóa chính trong JML
• Các tính năng nâng cao
• Đặc tả các ngoại lệ
• Thừa kế đặc tả
• Các trường model
• Đặc tả không hình thức
• Phép toán vị từ
• Cơ sở đặc tả hình thức
• Luật suy diễn
• Cơ sở toán học trong đặc tả hình thức
• Hệ thống phần mềm
• Lỗi phần mềm
• Ngôn ngữ và hệ thống
• Các ngôn ngữ đặc tả
• Kiểm tra mô hình
• Mô hình hóa dữ liệu
• Kiểu dữ liệu
• Đặc tả operation
• Dữ liệu kiểu mảng
• Kiểu đối tượng phức
• Kiểu tập hợp
• Design by contract
• Ngôn ngữ đặc tả
• Công cụ hỗ trợ
• Giới thiệu về ESC Java2
• Cách sử dụng và thuộc tính
• Cấu trúc của ESC
• Các file đặc tả
• Thủ thuật và cạm bẫy
• Đặc tả thừa kế
• Đặc tả sử dụng ánh xạ
• Kiểu ánh xạ
• Ngôn ngữ đặc tả Z
• Phép toán trên giản đồ