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

Bài giảng "Đặc tả hình thức - Chương 4: Số và kiểu mảng" cung cấp cho người học các kiến thức: Số và mảng là khái niệm quan trọng của Đặc tả hình thức, ngôn ngữ Z mô tả các dạng số - Đặc biệt là số tự nhiên dùng tương ứng với mảng. | Trường Đại học Công Nghệ Thông Tin ĐHQG-HCM Khoa Công Nghệ Phần Mềm Chương 4 Số và Kiểu mảng Giảng viên . Vũ Thanh Nguyên 4 5 2019 Thanh Nguyen https tailieudientucntt Nội Dung Số và mảng là khái niệm quan trọng của Đặc tả hình thức Ngôn ngữ Z mô tả các dạng số - đặc biệt là số tự nhiên dùng tương ứng với mảng 4 5 2019 Thanh Nguyen https tailieudientucntt 2 Kiểu Số Tập số nguyên Z -2 -1 0 1 2 Tập số tự nhiên N n Z n 0 0 1 2 Tập số nguyên dương N1 n Z n gt 0 1 2 4 5 2019 Thanh Nguyen https tailieudientucntt 3 Kiểu Số Tập số hữu tỉ Q x x m n m Z n Z 0 Tập số vô tỉ I x x m n m Z n Z 0 Tập số thực R Q I 4 5 2019 Thanh Nguyen https tailieudientucntt 4 Kiểu Số Các phép toán trên tập số nguyên 4 5 2019 Thanh Nguyen https tailieudientucntt 5 Kiểu Số Các phép toán trên số 4 5 2019 Thanh Nguyen https tailieudientucntt 6 Kiểu Số Ví dụ về hàm trả lại giá trị tuyệt đối của một số nguyên sử dụng sự miêu tả rỏ ràng như sau abs Z Z n Z n 0 abs n -n n 0 abs n n Hàm successor succ trả lại giá trị của số tiếp theo của số tự nhiên Succ 0 1 1 2 2 3 Hàm predecessor pred trả lại giá trị của số phía trước pred succ 4 5 2019 Thanh Nguyen https tailieudientucntt Kiểu Số Miền xác định của số Miền xác định giữa 2 số a b Z được xác định như sau a a 1 a 2 b-2 b-1 b Hoặc n Z a n b Nếu a gt b khi đó và a 4 5 2019 Thanh Nguyen https tailieudientucntt 8 Kiểu Số Cardinality Số phần tử của tập số nguyên Xác định là card hay ngôn ngữ z Ví dụ hay 0 a 1 4 5 2019 Thanh Nguyen https tailieudientucntt 9 Kiểu Số Cardinality Đối với miền xác định 1 b-a nếu a b 0 nếu a gt b max 0 1 b-a Vậy nó tương ứng là 1 2 3 b-a 1 b-a a a 1 a 2

• Kỹ thuật lập trình
• Bài giảng Đặc tả hình thức
• Đặc tả hình thức
• Lập trình phần mềm
• Công nghệ phần mềm
• Ngôn ngữ Z
• Số và kiểu mảng
• Kiểu dữ liệu
• Đặc tả hàm
• Đặc tả đệ quy
• Đặc tả hàm tường minh
• Đặc tả hàm không tường minh
• Đặ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
• Đặ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 đồ