Tiến Sĩ Nghiên cứu ứng dụng ngôn ngữ F* trong phát triển phần mềm

5



MỤC LỤC
LỜI CAM ĐOAN 3
LỜI CẢM ƠN 4
MỤC LỤC . 5
DANH MỤC CÁC KÝ HIỆU, THUẬT NGỮ, CHỮ VIẾT TẮT 7
DANH MỤC CÁC BẢNG 8
DANH MỤC CÁC HÌNH VẼ . 9
PHẦN MỞ ĐẦU . 10
Tính cấp thiết của đề tài 10
Mục tiêu của luận văn . 10
Công cụ phần mềm 10
Phương pháp nghiên cứu . 11
Bố cục luận văn . 11
CHƯƠNG 1: TỔNG QUAN VỀ LẬP TRÌNH HÀM 12
1.1 Giới thiệu chung về ngôn ngữ lập trình hàm 12
1.2 Các đặc điểm nổi bật của ngôn ngữ lập trình hàm 13
1.3 Sự phổ biến của ngôn ngữ lập trình hàm 14
1.4 Giới thiệu tổng quan về ngôn ngữ lập trình hàm F# . 15
CHƯƠNG 2: NGHIÊN CỨU LÝ THUYẾT VỀ NGÔN NGỮ F* 17
2.1. Giới thiệu chung . 17
2.1.1. Giới thiệu về ngôn ngữ F* . 17
2.1.2. Giới thiệu về kiểu phụ thuộc, hệ thống kiểu phụ thuộc . 17
2.2. Các đặc điểm nổi bật của ngôn ngữ F* 18
2.2.1. Ngôn ngữ tự chứng thực F* . 18
2.2.2. Trình biên dịch từ F* sang mã JavaScript . 19
2.3. Các khái niệm cơ bản khi lập trình với F* . 20
2.3.1. Các định nghĩa kiểu và loại thường dùng trong F* . 20
2.3.2. Các khái niệm chung về khai báo kiểu trong F* . 23 6



2.3.3. Lý thuyết về tập hợp: . 23
2.3.4. Định nghĩa, sử dụng mảng dữ liệu trong F* 24
2.3.5. Kiểu của số tự nhiên (NAT) 26
2.3.6. Chứng minh tính chất cơ bản trong F* 26
2.3.7. Loại suy luận và các ảnh hưởng tới tính toán 28
2.3.8. Sử dụng F* lập trình với các bài toán đơn giản . 29
2.3.9. Chứng minh bổ đề (Lemmas) 31
2.3.10. Chứng minh tính kết thúc của chương trình trong F* (Proving termination) . 35
2.4. Kết luận chương . 38
CHƯƠNG 3: BÀI TOÁN ỨNG DỤNG . 39
3.1. Ứng dụng F* vào các bài toán lập trình . 39
3.1.1. Ứng dụng trong bài toán sắp xếp mảng nổi bọt (Buble sort) 39
3.1.2. Ứng dụng trong lập trình sắp xếp mảng nhanh (Quick sort) . 40
3.1.3. Ứng dụng trong cái bài toán làm việc với các tập tin, thư mục . 45
3.2. Ứng dụng F* trong bài toán tính tổng tài nguyên sử dụng chương trình 48
3.2.1. Giới thiệu bài toán . 48
3.2.2. Giải quyết bài toán . 50
3.2.3. Tính toán giá trị mức giới hạn trên tổng chi phí tài nguyên cho chương trình . 57
KẾT LUẬN . 60
TÀI LIỆU THAM KHẢO . 61
PHỤ LỤC. CÁC CÔNG CỤ HỖ TRỢ CÀI ĐẶT THỰC NGHIỆM . 62