- Nghiên cứu ứng dụng ngôn ngữ F* trong phát triển phần mềm. - Tôi xin cam đoan luận văn này là công trình nghiên cứu của cá nhân tôi, dƣới sự hƣớng dẫn trực tiếp từ phía PGS.TS. - Kết quả cuối cùng đạt đƣợc của luận văn là thành quả của quá trình nghiên cứu bản thân, chƣa từng đƣợc công bố dƣới bất kỳ hình thức nào.. - Tôi xin chịu trách nhiệm về nghiên cứu trong luận văn.. - 10 Phƣơng pháp nghiên cứu. - Error! Bookmark not defined.. - CHƢƠNG 1: TỔNG QUAN VỀ LẬP TRÌNH HÀM. - 1.1 Giới thiệu chung về ngôn ngữ lập trình hàm. - 1.2 Các đặc điểm nổi bật của ngôn ngữ lập trình hàm. - 1.3 Sự phổ biến của ngôn ngữ lập trình hàm. - 1.4 Giới thiệu tổng quan về ngôn ngữ lập trình hàm F. - CHƢƠNG 2: NGHIÊN CỨU LÝ THUYẾT VỀ NGÔN NGỮ F. - Giới thiệu về ngôn ngữ F. - Giới thiệu về kiểu phụ thuộc, hệ thống kiểu phụ thuộc. - Các đặc điểm nổi bật của ngôn ngữ F. - Ngôn ngữ tự chứng thực F. - Các khái niệm cơ bản khi lập trình với F. - Sử dụng F* lập trình với các bài toán đơn giản . - Chứng minh tính kết thúc của chƣơng trình trong F* (Proving termination) Error! Bookmark not defined.. - CHƢƠNG 3: BÀI TOÁN ỨNG DỤNG. - Ứng dụng F* vào các bài toán lập trình. - Ứng dụng trong bài toán sắp xếp mảng nổi bọt (Buble sort. - Ứng dụng trong lập trình sắp xếp mảng nhanh (Quick sort. - Ứng dụng trong cái bài toán làm việc với các tập tin, thƣ mục. - Bookmark not defined.. - Ứng dụng F* trong bài toán tính tổng tài nguyên sử dụng chƣơng trình. - Giới thiệu bài toán. - Giải quyết bài toán. - 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 Error! Bookmark not defined.. - 1 F* Ngôn ngữ lập trình Fstar. - Bộ nhớ giao tác phần mềm, một giải pháp viết các chƣơng trình tƣơng tranh, thay cho cơ chế đồng bộ dựa trên khóa.. - 3 TFJ string Là một ngôn ngữ mở rộng của FJ tích hợp mô hình bộ nhớ giao tác phần mềm.. - 1 Type System Hệ thống kiểu. - 2 Transaction Giao tác. - 4 Binary Mã nguồn chƣơng trình. - 8 Onacid Trạng thái mở một giao tác. - 9 Commit Trạng thái kết thúc một giao tác. - 10 Lock-based synchronization Đồng bộ hóa dựa trên khóa 11 Nested transactions Các giao tác lồng. - 1 + m Mô tả thành phần + trong hệ thống kiểu dựa trên. - 2 − m Mô tả thành phần – trong hệ thống kiểu dựa trên. - 3 # m Mô tả thành phần # trong hệ thống kiểu dựa trên. - chuỗi số có dấu, m các giao tác lồng nhau.. - 4 ¬ m Mô tả thành phần ¬ thể hiện số lƣợng joint commit trong hệ thống kiểu dựa trên chuỗi số có. - Bảng 2.1: Khai báo biểu thức, kiểu, loại trong ngôn ngữ F. - Bảng 3.1 Bảng kết quả kiểm thử phép toán chính tắc chuỗi số có dấu. - Bảng 3.2 Bảng kết quả kiểm khử dấu. - Bảng 3.3 Bảng kết quả kiểm khử hàm merge. - Bảng 3.4 Bảng kết quả kiểm khử hàm joint commit. - Hình 2.1: Kết quả cho bài toán tính giai thừa. - Hình 2.2: Các kiểu, loại dữ liệu đƣợc sử dụng trong F* [4. - Hình 3.1: Kết quả cho bài toán sắp xếp nổi bọt. - Hình 3.2: Kết quả cho bài toán sắp xếp nhanh. - Hình 3.3: Ví dụ mô hình giao tác lồng, đa luồng và joint [13. - Trên thực tế, tùy theo yêu cầu của mỗi lĩnh vực mà chúng ta có thể lựa chọn các ngôn ngữ lập trình sao cho phù hợp. - Chúng ta có thể thấy rất nhiều ngôn ngữ lập trình đƣợc sử dụng ngày nay, trong đó phải kể đến một số ngôn ngữ lập trình rất đƣợc phổ biến nhƣ là Java, C#, Objective-C, JavaScript, SQL, PHP. - Các ngôn ngữ lập trình hàm nhƣ OCaml, ML, F#. - Ngôn ngữ lập trình hàm F# là ngôn ngữ có kiểu mạnh (strongly-typed) và tự suy luận kiểu (không cần phải khai báo kiểu cho các biến đầu vào), trình biên dịch có thể tự suy luận ra kiểu của các biến đầu vào đó khi dịch chƣơng trình. - Tuy nhiên các kiểu đƣợc sử dụng để gán cho các biến đầu vào của ngôn ngữ là có sẵn và đƣợc gán một cách tự động khiến ngƣời lập trình khó có thể tùy biến đƣợc trong F#.. - Từ nhu cầu này, ngôn ngữ F* đã ra đời. - Ngôn ngữ F* có hệ thống kiểu đƣợc xây dựng dựa trên nền tảng lý thuyết System Fω [1] nhƣng đƣợc mở rộng hơn với hệ thống kiểu phụ thuộc, các kiểu đƣợc tùy chỉnh, cho phép ngƣời lập trình có thể làm mịn kiểu dữ liệu cho chặt hơn, phù hợp hơn với ý đồ. - Ngoài ra F* có thể kiểm chứng tính đúng đắn của chƣơng trình theo kiểu dữ liệu mới đƣợc làm mịn này. - Tức là thông thƣờng, chúng ta chỉ có kiểu số nguyên (int) nhƣng với ngôn ngữ F* chúng ta có thể khai báo kiểu số nguyên nằm trong khoảng 0 đến 10, hay chỉ gồm các số chẵn hoặc chỉ có các số lẻ. - Hơn nữa ngôn ngữ F* có thể đƣợc dịch sang những ngôn ngữ khác nhƣ OCaml, F# hoặc JavaScript để thực thi. - Những vấn đề trên là cơ sở khoa học và thực tiễn để tôi thực hiện đề tài “Nghiên cứu ứng dụng ngôn ngữ F* trong phát triển phần mềm”.. - Trên cơ sở nghiên cứu lý thuyết, cài đặt, thử xây dựng các chƣơng trình cơ bản, luận văn đã ứng dụng ngôn ngữ F* vào việc xây dựng công cụ tính tổng tài nguyên đƣợc sử. - dụng trong chƣơng trình đa luồng có dùng bộ nhớ giao dịch, theo bài báo nghiên cứu của thầy hƣớng dẫn.. - Trong luận văn, tôi có sử dụng mã nguồn F* để cài đặt thuật toán chƣơng trình.. - Khanh, Lập Trình Hàm và Lập Trình Logic, Đà Nẵng, 2009.