ĐẠ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:

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

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)

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

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

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ố

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ư

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.


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

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

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].

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:
<inputid="number"type="text"/>

<divid="output"></div>

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*

Biểu thức
// Biểu thức

e ::=
| v// Biến số

| let x = e1 in e2// Ràng buộc trong hàm khác
| let rec f = v// Hàm gọi đệ quy
| match e with br1..brn// Tìm và kết hợp giá trị với biến hoặc biểu thức
| assert phi// khẳng định kiểm tra đúng
| raise e// Báo cáo ngoại lệ
| try e with br1..brn// Xử lý ngoại lệ

Top level
tl ::=val x : t
| open M// Mở thư viện
|
|

tdef// Định nghĩa kiểu
let [rec] x1 = e1
[and ... and xn = en]// Ràng buộc đệ quy lẫn nhau

Module
m ::= module M tl1 ... tln ;; e [end]

// Khai báo module


22

let z'' =(1-1=0). Trong các ngôn ngữ lập trình hàm như ML, lập trình
viên có thể chỉ cần định nghĩa int -> int tuy nhiên ở F*, để thể hiện ảnh hưởng của hàm
tới kết quả cần phải định nghĩa kết quả có dạngint-> Tot intgiống như ví dụ sau:
val is_positive :int->Totbool
let is_positive i = i > 0

Hoặc ta có thể định nghĩa 1 hàm với nhiều biến đầu vào như sau:
val min :int->int->Totint
let min i1 i2 = if i1> i2then i2else i1

Đối với một hàm xác định, giống với các ngôn ngữ lập trình khác, chúng ta cần khai
báo các kiểu giá trị cho một hàm, kết quả trả về và F* cũng vậy. Sử dụng val để khai báo
kiểu dữ liệu của một hàm, let để khai báo cho các hàm thực thi.
2.3.3. Lý thuyết về tập hợp:
Trong lý thuyết về tập hợp, F* sẽ cung cấp 1 cú pháp khá thú vị dành cho bộ dữ liệu.
như ví dụ sau:


24
type NTuple =
| Tuple_UU : 'a -> 'b ->('a * 'b)
| Tuple_UA : 'a::*-> 'b::A -> 'a -> 'b ->('a * 'b)

let f x = MkTriple.fst x + MkTriple.snd x + MkTriple.third x

2.3.4. Định nghĩa, sử dụng mảng dữ liệu trong F*
Ta có ví dụ như sau:
type iList :int=> S => S =
|INil : ilist 0 'a
|ICons : n:int-> ilist n 'a -> x:'a -> ilist (n +1) 'a

Kiểu iList Rất hữu ích và tối ưu bởi hai lý do sau đây. Đầu tiên, định nghĩa của
ngôn ngữ F* không cho phép viết như sau iList (-1)'a, điều đó là vô lý vì không có
danh sách có độ dài -1. Trong F*, việc nối 2 danh sách (string hoặc int) được thực hiện
kèm các ràng buộc tới kết quả trả về của hàm giống như đoạn chương trình dưới đây:
module AppendSumLengths
val length:list 'a -> Tot nat
letrec length l =match l with


25
|[]->0
|_::tl ->1+ length tl
val append : l1:list 'a -> l2:list 'a -> Tot (l:list 'a{length l = length l1
+ length l2})
letrec append l1 l2 =match l1 with
|[]-> l2
| hd::tl -> hd::append tl l2

Để kiểm tra được tính đúng đắn của chương trình trên, chúng ta định nghĩa cho hàm
nối danh sách với list 1 (l1) và list (l2) danh sách (l) sẽ có độ dài bằng 2 danh sách ban
đầu cộng lại. Thực vậy với l1 = {2,3} và l2 = {4}. Với vòng đầu tiên sẽ lấy ra giá trị 2 và
ghép tiếp với vòng lặp sau giá trị 3 và lấy từ danh sách l2 giá trị là 4. Vậy ta có danh sách