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

  • Số trang: 64 |
  • Loại file: PDF |
  • Lượt xem: 87 |
  • Lượt tải: 1
nguyetha

Đã đăng 7932 tài liệu

Mô tả:

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ VŨ QUANG HƯNG Nghiên cứu ứng dụng ngôn ngữ F* trong phát triển phần mềm LUẬN VĂN THẠC SĨCÔNG NGHỆ THÔNG TIN Hà Nội – 2015 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ VŨ QUANG HƯNG Nghiên cứu ứng dụng ngôn ngữ F* trong phát triển phần mềm Ngành: Chuyên ngành: Mã số: Công nghệ thông tin Kỹ thuật phần mềm 60480103 LUẬN VĂN THẠC SĨCÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS. TS. Trương Anh Hoàng NGƯỜI ĐỒNG HƯỚNG DẪN KHOA HỌC: TS. Nguyễn Như Sơn Hà Nội – 2015 3 LỜI CAM ĐOAN 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.Trương Anh Hoàng và TS. Nguyễn Như Sơn. Các số liệu, nội dung tham khảo được trích dẫn có nguồn gốc rõ ràng, tuân thủ tôn trọng quyền tác giả. 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. Hà Nội, ngày 28 tháng 5 năm 2015 Tác giả Vũ Quang Hưng 4 LỜI CẢM ƠN Để hoàn thành đề tài luận văn này, bên cạnh sự chủ động cố gắng của bản thân, tôi đã nhận được sự ủng hộ và giúp đỡ nhiệt tình từ các tập thể, cá nhân trong và ngoài trường. Qua đây, cho phép tôi được bày tỏ lòng cảm ơn sâu sắc tới thầy giáo PGS.TS.Trương Anh Hoàng, giảng viên bộ môn Công nghệ phần mềm trường Đại học công nghệ – Đại học Quốc gia Hà Nội, người đã trực tiếp động viên, định hướng và hướng dẫn tận tình trong quá trình học tập và hoàn thành đề tài luận văn này. Đồng kính gửi lời cảm ơn đến tập thể các thầy, cô giáo trong trường Đại học Công Nghệ – Đại học Quốc gia Hà Nội đã trau dồi kiến thức cho tôi, điều đó là nền tảng quí báu góp phần to lớn trong quá trình vận dụng vào hoàn thiện luận văn. Cuối cùng, tôi xin được gửi lòng biết ơn sâu sắc đến gia đình, bạn bè, đồng nghiệp đã tạo điều kiện về vật chất cũng như tinh thần, luôn sát cánh bên tôi, động viên giúp tôi yên tâm học tập và kết thúc khóa học. Xin chân thành cảm ơn! Tác giả Vũ Quang Hưng 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 7 DANH MỤC CÁC KÝ HIỆU, THUẬT NGỮ, CHỮ VIẾT TẮT CHỮ VIẾT TẮT, THUẬT NGỮ, KÝ HIỆU STT GIẢI NGHĨA CHỮ VIẾT TẮT 1 F* 2 STM (Software Transactional Memory) 3 TFJ string 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. 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. THUẬT NGỮ 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 Type System Transaction Thread Binary Type checker Stronglytyped AST (Abstract Syntax Tree) Onacid Commit Lock-based synchronization Nested transactions Multi-threaded Join Merge Spawn 16 Joint commits 17 Syntax Hệ thống kiểu Giao tác Luồng Mã nguồn chương trình Bộ kiểm tra kiểu Kiểu mạnh Cây cú pháp trừu tượng Trạng thái mở một giao tác Trạng thái kết thúc một giao tác Đồng bộ hóa dựa trên khóa Các giao tác lồng Đa luồng Hàm khử dấu trừ trong chuỗi có dấu chính tắc Hàm gộp 2 chuỗi có dấu chính tắc Sinh luồng Các commit của các luồng song song đồng thời thực hiện kết thúc một giao tác chung. Cú pháp KÝ HIỆU 1 + 2 − 3 # 4 ¬ m m m m Mô tả thành phần + trong hệ thống kiểu dựa trên chuỗi số có dấu, m thao tác onacid liên tiếp. Mô tả thành phần – trong hệ thống kiểu dựa trên chuỗi số có dấu, m thao tác commit liên tiếp. 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. 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ó 8 dấu. DANH MỤC CÁC BẢNG Bảng 2.1: Khai báo biểu thức, kiểu, loại trong ngôn ngữ F* ............................................. 20 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 .............................. 52 Bảng 3.2 Bảng kết quả kiểm khử dấu “−” thành dấu “¬” .................................................. 53 Bảng 3.3 Bảng kết quả kiểm khử hàm merge .................................................................... 54 Bảng 3.4 Bảng kết quả kiểm khử hàm joint commit .......................................................... 57 9 DANH MỤC CÁC HÌNH VẼ Hình 2.1: Kết quả cho bài toán tính giai thừa..................................................................... 20 Hình 2.2: Các kiểu, loại dữ liệu được sử dụng trong F* [4] .............................................. 22 Hình 3.1: Kết quả cho bài toán sắp xếp nổi bọt ................................................................. 40 Hình 3.2: Kết quả cho bài toán sắp xếp nhanh ................................................................... 45 Hình 3.3: Ví dụ mô hình giao tác lồng, đa luồng và joint [13] .......................................... 49 10 PHẦN MỞ ĐẦU Tính cấp thiết của đề tài Hiện nay ngành công nghiệp phần mềm đang rất phát triển ở nhiều lĩnh vực. 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ìnhrấ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# cũng dần được phổ biến trong khoảng thời gian gần đây. 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 đắncủ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ữangô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”. Mục tiêu của luận văn 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ệcxâ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. Công cụ phần mềm 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. Ngoài ra còn một số công cụ hỗ trợ như Cygwin, OCaml và Visual Studio (C#, F#). 11 Phương pháp nghiên cứu Để đề tài có thể đạt được kết quả như mục tiêu đặt ra, trong luận văn, tôi đã đề xuất và áp dụng các phương pháp nghiên cứu như sau: - Nghiên cứu các tài liệu liên quan đến lập trình hàm nói chung và lập trình ngôn ngữ F* nói riêng. - Thử nghiệm với một số chương trình cơ bảnsử dụng ngôn ngữ F*. - Ứng dụng xây dựng công cụ phần mềm: Cài đặt các thuật toán cho bài toán tính giá trị giới hạn trêntổng chi phí tài nguyên sử dụng của chương trình đa luồng có dùng bộ nhớ giao dịch trong trường hợp xấu nhất. Bố cục luận văn Trong luận văn này sẽ bao gồm các phần cơ bản sau: - Phần mở đầu: Đưa ra tính cấp thiết của đề tài, công cụ phần mềm được sử dụng, phương pháp nghiên cứu và bố cục của luận văn. - Chương 1: Giới thiệu tổng quan về ngôn ngữ lập trình hàm, đưa ra các đặc điểm nổi bật của ngôn ngữ lập trình hàm và giới thiệu về sự phổ biến của ngôn ngữ lập trình hàm trong ngành phát triển phần mềm hiện nay. - Chương 2: Giới thiệu tổng quan về ngôn ngữ F*,phương pháp xây dựng một chương trình trên nền tảng F*. Đưa ra các khái niệm, tính năng cơ bản và một số tính năng nâng cấp của F* so với các ngôn ngữ khác. Khái quát và tóm tắt lại để đưa ra kết luận chung về ngôn ngữ F*. - Chương 3: Ứng dụng F* trên một số bài toán lập trình trong thực tế.Tiến hành thực nghiệm và kiểm tra chương trình xây dựng bài toán tính giá trị giới hạn trên tổng chi phí tài nguyên của chương trình đối tượng bằng ngôn ngữ F*. Trình bày các thuật toán được sử dụng trong bài toán qua đó kết hợp các thuật toán lại với nhau để đưa ra kết quả cuối cùng cho bài toán. - Kết luận: Tổng hợp các kết quả đã đạt được, các vấn đề cần giải quyết và hướng mở rộng của đề tài. 12 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 Lập trình hàm là một mô hình lập trình trong đó việc tính toán là sự đánh giá của các hàm toán học, không sử dụng các trạng thái, dữ liệu biến đổi và các lệnh gán biến. Lập trình hàm nhấn mạnh việc ứng dụng các hàm số, trái với phong cách lập trình mệnh lệnh, nhấn mạnh vào sự thay đổi trạng thái [2]. Các ngôn ngữ lập trình hàm, đặc biệt là các loạn thuần về lập trình hàm có ảnh hưởng lớn trong giới học thuật hơn là dùng để phát triển các phần mềm thương mại. Mục đích của việc thiết kế ngôn ngữ lập trình hàm là mô phỏng các hàm toán học một cách nhiều nhất có thể. Trong lập trình hàm, biến là không cần thiết, như trong các bài toán học thường gặp. Trong logic toán học và khoa học máy tính, phép tính lambda là một hệ thống hình thức được sử dụng trong việc định nghĩa hàm số, ứng dụng hàm số và đệ quy. Phép tính lambda được phát triển để trở thành công cụ quan trọng trong việc nghiên cứu các vấn đề lý thuyết tính toán và lý thuyết đệ quy, và hình thành nên nền tảng cơ bản của mô hình lập trình hàm. Đôi khi người ta sử dụng các biểu thức lambda để biểu diễn cho các hàm không tên (ví dụ: λ(x) x * x thay thế cho binh_phuong(x) ≡ x*x). Các tham số của biểu thức lambda gọi là các tham số biến kết ghép. Khi biểu thức lamda được định trị với một tham số đã cho thì biểu thức được áp dụng cho tham số đó (Ví dụ (λ(x) x * x * x) (2) = 8). Hiện nay, ngôn ngữ lập trình hàm đang dần được phổ biến với sự phát triển đáng kể của ngôn ngữ F#. Ngôn ngữ F# có thể tận dụng hầu hết các công cụ phát triển trong Visual Studio. F# hỗ trợ lập trình hướng đối tượng. Khi lập trình với F#, các đoạn mã được viết ra cũng đơn giản hơn so với các ngôn ngữ như C# hoặc Java tuy nhiên điều khó khăn nhất đối với những lập trình viên chưa biết về lập trình hàm đó chính là cú pháp hoàn toàn mới của nó, gần như sẽ rất khác so với PHP, Java, C. Tại sao ngôn ngữ lập trình hàm lại xứng đáng để bạn bỏ thời gian để học và làm việc? Nếu là lập trình viên với nhiều đam mê thì ngôn ngữ lập trình hàm sẽ khơi gợi sự tò mò theo một cách nào đó. Trong lập trình hàm, lập trình viên sẽ làm việc thường xuyên hơn với các hàm hồi quy và quên đi các hàm như if else, while, do. Việc lập trình nêu trên có thể khiến lập trình viên cảm thấy khó khăn hơn rất nhiều, tuy nhiên khi đã quen với nó, bạn sẽ thấy kỹ năng lập trình của mình ở một trình độ cao hơn. Ngoài ra, trong các hàm được viết ra, với các dữ liệu đầu vào thì bạn chỉ có duy nhất một đầu ra mà thôi. Các khả năng có thể xảy ra đều được trình biên dịch đánh giá và báo lỗi cho lập trình viên. 13 1.2 Các đặc điểm nổi bật của ngôn ngữ lập trình hàm Hệ thống kiểu có thể biết đến là đặc điểm nổi bật nhất trong ngôn ngữ lập trình hàm. Trong F#, việc khai báo kiểu của biến là hoàn toàn không cần thiết. Khi định nghĩa một biến và gán giá trị cho nó, trình biên dịch sẽ tự suy luận ra biến đó sẽ sử dụng kiểu gì và gán cho biến. Tương tự như vậy, khi khai báo một hàm, lập trình viên có thể cân nhắc xem có cần khai báo kiểu dữ liệu đầu vào và kiểu dữ liệu trả về hay không vì sau khi định nghĩa các hàm tính toán, F# sẽ tự suy luận ra kiểu của các hàm đó. Việc sử dụng các kiểu dữ liệu đại số và so sánh với mẫu làm cho việc thao tác trên các cấu trúc dữ liệu phức tạp trở nên thuận tiện và rõ ràng hơn. Sự tồn tại của việc kiểm tra kiểu mạnh mẽ trong thời gian biên dịch khiến cho các chương trình trở nên đáng tin cậy hơn, việc luận kiểu cũng giúp lập trình viên không cần khai báo thủ công các kiểu để biên dịch. Một số ngôn ngữ lập trình hàm định hướng nghiên cứu được biết đến hiện nay như Coq [3], Agda [4]. Các kiểu được sử dụng trong các ngôn ngữ trên được gọi là các kiểu phụ thuộc. Các kiểu phụ thuộc này có thể được mô tả bằng các mệnh đề tự do trong logic mệnh đề. Các chương trình có kiểu tốt (well-typed) trong những ngôn ngữ nêu trên sẽ trở thành phương tiện cho việc viết các hàm chứng minh toán học hình thức mà từ đó trình biên dịch sẽ sinh ra các mã được chứng nhận. Ngoài ra, một đặc điểm khác có thể kể đến trong lập trình hàm đó là việc sử dụng đệ quy. Vòng lặp trong các ngôn ngữ lập trình hàm thường được thực hiện thông qua đệ quy. Hàm đệ quy sẽ tự gọi chính nó, cho phép thực hiện đi thực hiện lại một tác vụ. Đa số các ngôn ngữ lập trình hàm đa mục đích đều cho phép đệ quy không giới hạn, tuy nhiên việc đó có thể gây ra sự thiếu căn cứ cho việc suy diễn công thức, đòi hỏi phải có các khái niệm không nhất quán trong logic do hệ thống kiểu của ngôn ngữ quy định. Các chương trình trong lập trình hàm là các định nghĩa hàm và các áp dụng hàm. Sự thực hiện là việc đánh giá các áp dụng hàm trong đó một hàm luôn cho cùng một kết quả trả về khi ta gán cho nó cùng một đối số ví dụ như f(x) + f(x) và 2*f(x) luôn cùng một kết quả. Ngoài ra, ngữ nghĩa của ngôn ngữ lập trình hàm đơn giản hơn ngữ nghĩa của ngôn ngữ lập trình mệnh lệnh. Trong các ngôn ngữ lập trình hàm, các lời gọi chương trình con được viết thành biểu thức đơn giản. Các ngôn ngữ hàm cũng là các ngôn ngữ bậc cao và mang tính trừu tượng hơn so với các ngôn ngữ mệnh lệnh. Ngoài ra, lập trình hàm thường tránh sử dụng các biến toàn cục, trong khi đó, việc sử dụng biến toàn cục của người lập trình mệnh lệnh là cần thiết và nên dùng. Khi lập trình với ngôn ngữ hàm, người lập trình cần phải định nghĩa các hàm toán học dễ suy luận, dễ hiểu mà không cần quan tâm chúng được cài đặt 14 như thế nào ở trong máy. Mặt khác, trong ngôn ngữ mệnh lệnh, việc thay đổi trạng thái toàn cục được cho rằng hoàn toàn bất lợi. Nhiều phần khác nhau của chương trình tác động không trực tiếp lên các biến và do vậy làm cho chương trình khó hiểu. Các thủ tục thường được gọi sử dụng ở các phần khác nhau của chương trình gọi nên rất khó xác định các biến bị thay đổi như thế nào sau lời gọi. Như vậy, sự xuất hiện hiệu ứng phụ làm cản trở việc chứng minh tính đúng đắn (correctness proof), cản trở tối ưu hóa (optimization), và cản trở quá trình song song tự động (automatic parallelization) của chương trình[5]. Bên cạnh những tính ưu việt, ta cũng cần xem xét những bất lợi của lập trình hàm: Thứ nhất đó là thiếu các lệnh gán và các biến toàn cục, thứ hai đó là có sự khó khăn trong việc mô tả các cấu trúc dữ liệu và khó để kiểm soát quá trình vào ra của dữ liệu. Một vấn đề khác gây khó khăn cho lập trình viên đó là rất khó để thay đổi một cấu trúc dữ liệu trong mảng. Trong ngôn ngữ mệnh lệnh, sự thay đổi một phần tử mảng rất đơn giản. Tuy nhiên trong ngôn ngữ lập trình hàm, một mảng không thể bị thay đổi. Người ta cần sao chép mảng, loại bỏ những phần tử sẽ bị thay đổi và thay thế ngay lập tức các giá trị mới cho phần tử này. Cách tiếp cận này kém hiệu quả hơn so với phép gán cho phần tử [5]. Kết luận lại, các ngôn ngữ hàm dựa trên việc tính giá trị của các biểu thức, các biến toàn cục và phép gán kiểu bị loại bỏ, giá trị được tính bởi một hàm phụ thuộc vào các tham đối, tuy nhiên thông tin trạng thái được đưa ra tưởng minh nhờ các tham đối của hàm và kết quả [5]. 1.3 Sự phổ biến của ngôn ngữ lập trình hàm Các ngôn ngữ lập trình hàm hiện nay được biết đến khá nhiều và một trong số đó có thể kể đến là F#. Ngôn ngữ F# được cài đặt bởi tiến sĩ Don Syme tại Microsoft Research tại Cambridge. Hiện tại được tiếp quản bởi Microsoft và vẫn đang được tiếp tục phát triển bởi nhóm chuyên gia ở cả Cambridge và Redmond. Ngôn ngữ F# mang đến cho bạn một ngôn ngữ lập trình hàm an toàn, gọn nhẹ mà hiệu quả. Theo giấy phép chia sẻ nguồn của Microsoft, các đoạn mã nguồn được cung cấp sẵn cho lập trình viên. Microsoft cho phép tải về miễn phí trình biên dịch dưới dạng phiên bản nhị phân như là một gói phần mềm độc lập hoặc là một bộ cài cho Visual Studio. Với việc phát hành phiên bản F# 2.0, F# 3.0 và mới nhất là F# 4.0, nhóm phát triển sẽ chuyển sang mô hình mới mà họ gọi là thả mã (Code drop) trong đó phiên bản mới của trình biên dịch và các thư viện sẽ được phát hành cùng với phiên bản mới của ngôn ngữ. Mã này hiện diện như là một phần của F# PowerPack. Hiện nay, F# phiên bản 4.0 đã được cài đặt mặc định với Visual Studio 2015 vàF# có thể chạy trên phần lớn các nền tảng như HTML5, Android, JavaScript, Windows và MacOS. 15 1.4 Giới thiệu tổng quan về ngôn ngữ lập trình hàm F# Như đã nhắc đến ở các phần trên, việc lập trình với ngôn ngữ F# khá là khác biệt so với các ngôn ngữ lập trình hiện nay như C#, Java. Chúng ta có thể xem qua một số đoạn mã sau đây để thấy được sự khác biệt của ngôn ngữ này: module AppendList letrec append l1 l2 = match l1 with | [] -> l2 | hd::tl -> hd::append tl l2 let l1 = [1;2;3] let l2 = [9;4;5] printfn"%A" (append l1 l2) System.Console.ReadLine() |> ignore Trên đây là một ví dụ đơn giản về việc ghép hai mảng dữ liệu lại với nhau. Trong lập trình hàm, việc khai báo kiểu cho một hàm hầu như là không cần thiết. Trình biên dịch sẽ tự suy luận kiểu cho hàm append trên và sẽ có dạng như sau: 'a list -> 'a list -> 'a listtrong đó chúng ta có thể tùy ý gán các dữ liệu cho các mảng l1 và mảng l2. Như vậy mảng dữ liệu có thể có của hàm trên như sau: let l1 = ["a";"b";"c"] let l2 = ["d";"e";"f"] Việc quyết định kiểu dữ liệu cho hàm sẽ tùy vào việc định nghĩa mảng dữ liệu nào trước. Chúng ta định nghĩa l1 là mảng chuỗi kí tự thì l2 cũng phải là mảng chuỗi kí tự chứ không thể là chuỗi số tự nhiên được. Ngôn ngữ F# sử dụng thư viện .NET cũng giúp cho việc lập trình với F# trở nên dễ dàng hơn. Các thư viện khi lập trình với F# như System.IO, Microsoft.FSharp.Text.Lexing, Microsoft.FSharp.Text.Parsing.ParseHelpers và Microsoft.FSharp.Collections giúp ích rất nhiều trong các bài toán như đọc ghi dữ liệu, phân tích cú pháp trong một đoạn mã cho trước. Mặt khác trong ngôn ngữ F#, chúng ta có thể tự khai báo một số kiểu mới cho chương trình ví dụ như đoạn mã dưới đây: type | | | | type type type | Tag = Plus = 0 Minus = 1 Max = 2 Join = 3 TagNum = Tag * int TagSeq = TagNum list Tree = Branch of Tree list 16 | Leaf of TagNum Ở đây chúng ta có thể khai báo một kiểu dữ liệu mới đó là Tag. Trong kiểu Tag chứa các giá trị có thể có như Plus, Minus, Max, Join. Tiếp theo chúng ta khai báo một kiểu khác là TagNum được hiểu nôm na là 1 cặp gồm kiểu Tag và số tự nhiên (Ví dụ: (Plus, 1), (Minus,3), (Max,4)). Kiểu TagSeq là kiểu danh sách bao gồm mảng dữ liệu mà trong đó các phần tử có kiểu là TagNum. Không chỉ dừng lại ở đó, khi làm việc với F#, chúng ta có thể khai báo và làm việc với cây cú pháp trừu tượng giống như các ngôn ngữ lập trình khác và cao cấp hơn, chúng ta có thể định nghĩa kiểu dữ liệu cho gốc và lá của cây cú pháp này. Chúng ta có thể xây dựng nên cây cú pháp này theo như ví dụ sau: letrec addTree lst1 = match lst1 with | [] -> [] | '-'::xs-> List.append [Leaf (Tag.Minus, 1)] (addTree xs) | '+'::xs-> List.append [Leaf (Tag.Plus, 1)] (addTree xs) | '('::xs-> [Branch (addTree xs)] | ')'::xs-> addTree xs | x::xs -> addTree xs Với giá trị đầu vào của mảng l1 là['(';'+';'1';'-';'2';')';'-';'1']ta sẽ có cây cú pháp có dạng như sau: [Branch [Leaf (Plus,1); Leaf (Minus,2)];Leaf (Minus,1)]. Như vậy chúng ta có thể thấy rằng việc sử dụng ngôn ngữ lập trình hàm rất trực quan và giúp ích cho lập trình viên rất nhiều trong việc tự suy luận kiểu của hàm. Qua một số ví dụ về lập trình với F#, ta có thể thấy rằng việc lập trình với ngôn ngữ này khá là đơn giản với cú pháp rõ ràng, các hàm được xây dựng có tính tổng quát cao. Mặt khác, việc hỗ trợ xây dựng kiểu cũng là một điểm khá thú vị trong ngôn ngữ lập trình hàm này. Một ngôn ngữ lập trình hàm mới, kế thừa gần như toàn bộ các tính năng của F#, tuy nhiên bổ sung thêm việc khai báo các kiểu tùy chỉnh tinh vi hơn so với kiểu gốc, các chức năng xác thực tính đúng đắn của đoạn mã chương trình và đang được phát triển hiện nay đó chính là ngôn ngữ F*. Các chương dưới đây sẽ giới thiệu cái nhìn chung nhất, các đặc điểm và một số bài toán áp dụng khi lập trình với ngôn ngữ F*. 17 CHƯƠNG 2: NGHIÊN CỨU LÝ THUYẾT VỀ NGÔN NGỮ F* 2.1. Giới thiệu chung 2.1.1. Giới thiệu về ngôn ngữ F* Fstar (F*) [2] là ngôn ngữ lập trình hàm có thể xác thực tính đúng đắn của các đoạn mã viết ra, được phát triển bởi trung tâm nghiên cứu của Microsoft, MSR-Inria, Inria và trung tâm phần mềm IMDEA. Với các phương thức và cách hoạt động gần giống với F7 [5], Coq [6], Agda [7] và một số ngôn ngữ ML [3] khác, F* có đầy đủ các tính năng của lập trình hàm như hệ thống kiểu, tính chặt chẽ, và là một ngôn ngữ lập trình bậc cao. Hệ thống kiểu của F sao đa dạng phong phú hơn các ngôn ngữ sử dụng hệ thống kiểu phụ thuộc (dependent type) [4] khác ở chỗ nó cho phép người sử dụng đặc tả chính xác hơn về thông tin kiểu của biến và kiểu dữ liệu trả về của một hàm trong chương trình. Các đặc tả trên sẽ được trình biên dịch kiểm tra một cách bán tự động về tính đúng đắn của chúng. Nhờ vậy, nó thường được thiết kế để xây dựng các hệ thống có tính an toàn và độ tin cậy cao. Mặc dù là một ngôn ngữ mới nhưng người dùng có thể thiết lập, cài đặtF* một cách dễ dàng với tốc độ biên dịch khá nhanh. Mã nguồn của F* là mở và có thể chạy trên nhiều hệ điều hành. Chúng ta có thể tải bản cài đặt (binary) của trình biên dịch F* trên Windows, Linux hoặc MacOS hay có thể tự mình xây dựng trình biên dịch F* từ mã nguồn mở trên github. Bên cạnh đó, người dùng có thể dễ dàng lập trình với ngôn ngữ F* bởicú pháp, câu lệnh khi lập trình bằng ngôn ngữ này khá giống với F#, một ngôn ngữ khá phổ biến trong Visual Studio của Microsoft. Tuy nhiên cho đến nay, ngôn ngữ F* chưa thể chạy trực tiếp các đoạn mã được viết sẵn mà chỉ dừng lại ở việc xác thực tính đúng đắn của các đoạn mã trên. Chính vì vậy, F* hỗ trợ chuyển đổi các đoạn mã F* sang OCaml hoặc F#, JavaScript để lập trình viên có thể chạy hoặc gỡ lỗi chương trình được một cách linh hoạt hơn. Điều đó đòi hỏi người dùng cần phải tìm hiểu thêm về các ngôn ngữ khác trong quá trình sử dụng F*. 2.1.2. Giới thiệu về kiểu phụ thuộc, hệ thống kiểu phụ thuộc Để hiểu rõ hơn về ngôn ngữ F*, sau đây tôi sẽ giải thích một số khái niệm về kiểu phụ thuộc và hệ thống kiểu phụ thuộc. Kiểu phụ thuộc: Kiểu phụ thuộc[8] là kiểu mà phụ thuộc vào giá trị của các kiểu khác[9]. 18 Ví dụ: - Kiểu An là kiểu mảng gồm n phần tử mà các phần tử mang kiểu A. - Kiểu Am * n là một ma trận có kích thước m*n với các phần tử có kiểu là A. Hệ thống kiểu phụ thuộc: Hệ thống kiểu phụ thuộc là phương pháp phân tích tĩnh dựa trên các quy tắc kiểu được định nghĩa để đưa ra các khẳng định chương trình có xây dựng đúng không và cũng hạn chế các rủi ro có thể xảy ra. Hệ thống kiểu có thể biết chính xác việc sử dụng các giá trị gán cho biến hoặc hàm mà không cần thực thi nó [10]. Các ngôn ngữ lập trình với hệ thống hỗ trợ kiểu phụ thuộc: - Agda (programming language) ATS (programming language) Cayenne (programming language) Epigram (programming language) F* (programming language) Idris (programming language) 2.2. Các đặc điểm nổi bật của ngôn ngữ F* 2.2.1. Ngôn ngữ tự chứng thực F* Ngôn ngữ tự chứng thực (Self Certification) là ngôn ngữ có khả năng kiểm chứng tính đúng đắn của các chương trình được xây dựng bởi ngôn ngữ đó. Một số ngôn ngữ trước đó cũng có khả năng này như Coq [11], Agda[7]. Trình biên dịch F* có thể tự kiểm chứng tính đúng đắn của các chương trình xây dựng bằng F*. Hơn nữa trình biên dịch F* lại được xây dựng bằng ngôn ngữ F* nên có thể sử dụng trình biên dịch của F* để kiểm chứng đúng những đoạn mã xây dựng ra trình biên dịch này.Khi thử tự kiểm chứng kiểu trên F* và chứng thực đúng những kiểu đó trên Coq, chúng ta có một kết quả tương đương [11]. Điều đó chứng tỏ rằng, bộ kiểm tra kiểu trong trình biên dịch của F* hoàn toàn có thể cho một kết quả chính xác. Mặt khác trong tương lai, ngôn ngữ F* còn có khả năng sử dụng linh hoạt trên các máy tính cá nhân và đặc biệt là trong các đoạn mã dành cho di động, nơi mà Coq không khả dụng. 19 2.2.2. Trình biên dịch từ F* sang mãJavaScript 2.2.2.1. Giới thiệu Nhiều công cụ lập trình hiện nay cho phép các lập trình viên phát triển các ứng dụng của họ ở các ngôn ngữ bậc cao và đưa chúng lên web thông qua trình biên dịch JavaScript[12].Trong khi thực tế và sử dụng, không có sự đảm bảo nào cho tính xác thực của các trình biên dịch đó, không có tính an toàn cho các chương trình thực thi với JavaScript. Tuy nhiên khi kết hợp giữa trình biên dịch F* và JavaScript,lập trình viên có thể triển khai một cách hiệu quả các đoạn mã của mình so với việc chỉ sử dụng đơn thuầnJavaScript[13] do F* có khả năng tự chứng thực tính đúng đắnvà đảm bảo độ bảo mật thông tin của chương trình được viết. Đến đây, ngoài khả năng tự chứng thực như đã trình bày ở trên, chúng ta bắt gặp ưu điểm hỗ trợ bảo mật thông tin của ngôn ngữ F*. Thư viện như jQuery và Prototype đang được sử dụng rất phổ biến, cung cấp các khả năng hỗ trợ cho thiết kế website nhưng chỉ làm bằng cách sử dụng các tính năng của JavaScript. Như vậy chỉ cần thay đổi một số thông tin viết bằng JavaScript trên website, kẻ xấu có thể lấy được thông tin của người dùng. Tuy nhiên khi sử dụng với F*, một số thông tin khiến kẻ xấu khó có thể khai thác như tính kiểu của biến đầu vào, khả năng tự kiểm tra tính đúng đắn của hàm nếu có sự thay đổi, chứng minh bằng các bổ đề định nghĩa trước cho các hàm thực thi trong chương trình. F* đánh giá đoạn mã được xây dựng dựa trên các chương trình mẫu và các thư viện an toàn [4]. 2.2.2.2. Triển khai F* trong các trình duyệt web thông qua JavaScript Ví dụ sau đây sẽ cho ta thấy làm sao để sử dụng ngôn ngữ F* kết hợp với JavaScript trên nền web. Sử dụng F* cho bài toán tính giai thừa trên nền web, người sử dụng có thể nhập số nguyên vào ô văn bản có sẵn và bấm“CalculateFactorial!” để có được kết quả. 1 2 3 4 5 6 7 8 9 10 11 module Factorial open DOM val factorial:nat->nat letrec factorial n = if(n =0)then1 else n *(factorial (n -1)) let doit ()=match DOM.getElementById "number"with |None->() |Some elt -> let n = string2num (elt.getValue())in match DOM.getElementById "output"with 20 12 |None->() 13 |Some elt -> elt.setInnerText (concat_l ["Factorial of "; num2string n;" is ";num2string (factorial n)]) Đoạn mã từ dòng 3 đến dòng 6 định nghĩa hàm tính giai thừa với việc khai báo kiểu dữ liệu cho hàm tại dòng 3 và hàm tính toán từ dòng 4 đến dòng 6. Hàm để thực thi lấy dữ liệu và trả về kết quả trên web từ dòng 7 đến dòng 13. Tại dòng 7, hàm tìm phần tử có id là number trên trang web, nếu có phần tử đó, thực hiện tiếp việc lấy dữ liệu trong phần tử trên. Sau đó tại dòng 11, hàm tiếp tục tìm kiếm phần tử có id là output, nếu có hàm sẽ thực hiện gán kết quả cho phần tử đó là giá trị giai thừa tìm được. Chúng ta có đoạn mã nhúng HTML cho đoạn mã trên như sau:
Ta sẽ có kết quả như sau: Hình 2.1: Kết quả cho bài toán tính giai thừa Như vậy thay vì ta viết một đoạn mã JavaScript để tính giai thừa thì ta có thể viết một hàm bằng ngôn ngữ F* và có thể làm được công việc tương tự. Lập trình viên có thể sử dụng tính năng --codegen của trình biên dịch F* để triển khai các đoạn mã sau khi đã viết trên các ngôn ngữ khác nhau như JavaScript, F#, OCaml. Tuy nhiên tại thời điểm hiện tại, trình biên dịch mới chỉ giới hạn tính năng -- codegen từ F* sang các đoạn mã OCaml. 2.3. Các khái niệm cơ bản khi lập trình với F* 2.3.1. Các định nghĩa kiểu và loại thường dùng trong F* Sau đây chúng ta sẽ tìm hiểu một số khái niệm lập trình cơ bản, các từ khóa cần biết đến khi lập trình với ngôn ngữ F*: Bảng 2.1: Khai báo biểu thức, kiểu, loại trong ngôn ngữ F* Cú pháp: i ::= 0 | 1 | -1 | ... Loại // Khai báo số nguyên
- Xem thêm -