ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
TRẦN MẠNH ĐÔNG
NGHIÊN CỨU KỸ THUẬT PHÂN TÍCH CHƯƠNG TRÌNH
TĨNH TRONG VIỆC NÂNG CAO CHẤT LƯỢNG PHẦN MỀM
LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
Hà Nội – 2013
ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
TRẦN MẠNH ĐÔNG
NGHIÊN CỨU KỸ THUẬT PHÂN TÍCH CHƯƠNG TRÌNH
TĨNH TRONG VIỆC NÂNG CAO CHẤT LƯỢNG PHẦN MỀM
Ngành: Công nghệ thông tin
Chuyên ngành: Công nghệ phần mềm
Mã số: 60 48 10
LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. Nguyễn Trường Thắng
Hà Nội – 2013
Ph
3
Mục lục
LỜI CÁM ƠN
1
LỜI CAM ĐOAN
2
MỤC LỤC
3
DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT
5
DANH MỤC CÁC HÌNH VẼ
6
MỞ ĐẦU
7
1 Giới thiệu
9
1.1 Giới thiệu về phân tích chương trình . . . . . . . . . . . . . . . . . . .9
1.2 Điểm mạnh và điểm yếu . . . . . . . . . . . . . . . . . . . . . . . . 10
.
1.3 Các công nghệ phân tích chương trình tĩnh . . . . . . . . . . . . . . . 10
.
1.4 Nền tảng . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
.
1.4.1 Đồ thị luồng điều khiển . . . . . . . . . . . . . . . . . . . . . 12
.
1.4.2 Lý thuyết Dàn . . . . . . . . . . . . . . . . . . . . . . . . . . 15
.
1.4.3 Thuật toán điểm cố định . . . . . . . . . . . . . . . . . . . . . 21
.
2 Phân tích chương trình tĩnh
24
2.1 Phân tích luồng dữ liệu nội thủ tục . . . . . . . . . . . . . . . . . . . 24
.
2.1.1 Phân tích quay lại (backward) . . . . . . . . . . . . . . . . . . 25
.
2.1.2 Phân tích chuyển tiếp (forward) . . . . . . . . . . . . . . . . . 31
.
2.2 Phân tích luồng dữ liệu liên thủ tục . . . . . . . . . . . . . . . . . . . 40
.
2.2.1 Xây dựng đồ thị luồng dữ liệu . . . . . . . . . . . . . . . . . . 41
.
2.2.2 Tính cảm ngữ cảnh (context sensitivity) . . . . . . . . . . . . . 43
.
2.2.3 Ứng dụng phân tích luồng dữ liệu liên thủ tục . . . . . . . . . 45
.
4
3 Thực nghiệm
47
3.1 Tổng quan về SOOT . . . . . . . . . . . . . . . . . . . . . . . . . . 47
.
3.1.1 Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
.
3.2 Phân tích chương trình cùng với SOOT trong Eclipse . . . . . . . . . 48
.
KẾT LUẬN
52
TÀI LIỆU THAM KHẢO
53
PHỤ LỤC A
55
PHỤ LỤC B
57
PHỤ LỤC C
60
PHỤ LỤC D
62
5
DANH MỤC CÁC KÝ HIỆU VÀ CHỮ VIẾT TẮT
CFG
Control Flow Graph
CNPM Công nghệ phần mềm
CNTT Công nghệ thông tin
DFA
Data Flow Analysis
6
Danh sách hình vẽ
1.1 CFG cho các lệnh cơ bản. . . . . . . . . . . . . . . . . . . . . . . . 13
.
1.2 CFG cho các lệnh tuần tự. . . . . . . . . . . . . . . . . . . . . . . . 13
.
1.3 CFG cho các lệnh if, if-else. . . . . . . . . . . . . . . . . . . . . . . 13
.
1.4 CFG cho các lệnh while, for. . . . . . . . . . . . . . . . . . . . . . . 14
.
1.5 CFG của chương trình tính giai thừa. . . . . . . . . . . . . . . . . . . 15
.
1.6 Biểu đồ Hasse biểu diễn Dàn. . . . . . . . . . . . . . . . . . . . . . 16
.
1.7 Các biểu đồ Hasse là Dàn. . . . . . . . . . . . . . . . . . . . . . . . 17
.
1.8 Các biểu đồ Hasse không phải là Dàn. . . . . . . . . . . . . . . . . . 17
.
1.9 Phép toán cộng dàn. . . . . . . . . . . . . . . . . . . . . . . . . . . 19
.
1.10 Phép toán nâng (lift) dàn. . . . . . . . . . . . . . . . . . . . . . . . . 19
.
1.11 Phép toán lift của các tập tạo thành dàn. . . . . . . . . . . . . . . . . 20
.
2.1 Dàn cho chương trình phân tích tính sống của biến. . . . . . . . . . . 26
.
2.2 Dàn cho chương trình phân tích biểu thức bận rộn. . . . . . . . . . . 29
.
2.3 CFG của chương trình phân tích biểu thức bận rộn. . . . . . . . . . . 30
.
2.4 Dàn cho chương trình phân tích biểu thức có sẵn. . . . . . . . . . . . 34
.
2.5 CFG của chương trình phân tích biểu thức có sẵn. . . . . . . . . . . . 34
.
2.6 CFG của chương trình phân tích định nghĩa tới được. . . . . . . . . . 38
.
2.7 Đồ thị def-use định nghĩa tới được của các biến của chương trình. . . 40
.
2.8 Ví dụ CFG tổng quát cho chương trình có chứa lời gọi hàm. . . . . . 42
.
2.9 CFG của chương trình phân tích liên thủ tục. . . . . . . . . . . . . . 43
.
2.10 CFG đơn biến. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
.
2.11 CFG đa biến. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
.
3.1 Tổng quan về luồng làm việc của SOOT [10] . . . . . . . . . . . . . 48
.
3.2 Phương thức copy() và merge() trong SOOT . . . . . . . . . . . . . . 49
.
3.3 Kết quả phân tích với SOOT . . . . . . . . . . . . . . . . . . . . . . 51
.
7
MỞ ĐẦU
Sự tiến hóa nhanh chóng của các thiết bị phần cứng trong hơn 30 năm qua đã
đưa đến hệ quả về sự phát triển theo cấp số nhân của kích cỡ các chương trình
phần mềm chạy trên đó. Quy mô của những ứng dụng cực lớn này (khoảng từ 1
tới 40 triệu dòng mã lệnh) vẫn tiếp tục gia tăng trong thời gian tới. Những phần
mềm như thế cần phải được thiết kế với chi phí vừa phải trong khi vẫn phải bảo trì,
nâng cấp trong toàn bộ vòng đời của chúng, tầm 20 năm. Một thực tế là quy mô
và hiệu quả của những nhóm lập trình và bảo trì chúng không thể tăng theo tỉ lệ
như vậy. Với hoàn cảnh đó, tỉ lệ giả định 1 lỗi trong 1000 dòng lệnh đối với những
phần mềm như vậy là quá lạc quan và sẽ không thể đạt được trong những hệ thống
đòi hỏi độ an toàn cực cao. Do đó, vấn đề về độ tin cậy của phần mềm (software
reliability) chắc chắn là một mối quan tâm và thách thức đối với xã hội hiện đại
ngày càng phụ thuộc vào các dịch vụ do máy tính đem lại. Nhiều kỹ thuật kiểm
chứng phần mềm (software verification) và các công cụ hỗ trợ đi kèm đã được phát
triển để thực thi hoặc giả lập chương trình trên nhiều môi trường khác nhau. Tuy
nhiên, gỡ rối mã dịch hoặc giả lập mô hình của mã nguồn các chương trình không
thể mở rộng quy mô và thường chỉ xét được mức độ bao phủ hạn chế các hành
vi động của chương trình. Các phương pháp hình thức trong kiểm chứng chương
trình (formal methods) cố gắng chứng minh một cách tự động rằng chương trình
sẽ thực thi đúng đắn trên mọi môi trường được đặc tả. Mảng nghiên cứu này bao
gồm các phương pháp suy dẫn (deductive methods), kiểm chứng mô hình (model
checking), định kiểu chương trình (program typing) và phân tích chương trình tĩnh
(static program analysis). Ba nhóm đầu tập trung vào việc kiểm chứng phần mềm
tại mức mô hình, trong khi nhóm cuối cùng xử lý phần mềm tại mức mã nguồn.
Phân tích chương trình tĩnh thu hút sự quan tâm nhất do nền tảng lý thuyết hình
thức của nó cũng như mục đích của nó đối với các ứng dụng của nó trong thực tế.
Kỹ thuật này phát hiện tính chất/hành vi của một chương trình mà không yêu cầu
chạy chương trình đó. Ngoài ra, một số lỗi chương trình như việc khởi tạo/sử dụng
biến chương trình, biến con trỏ NULL,... có thể được phát hiện bởi kỹ thuật này.
Mục tiêu chính của luận văn là cập nhật được những xu thế trên thế giới trong
lĩnh vực phân tích chương trình và cải tiến những kỹ thuật này. Cụ thể, luận văn
tập trung vào nghiên cứu kỹ thuật phân tích chương trình dựa trên đồ thị luồng
dữ liệu để nâng cao chất lượng phần mềm. Tiến hành thực nghiệm trên công cụ
8
SOOT, một công cụ mã nguồn mở phân tích chương trình viết bằng Java trên môi
trường tích hợp phát triển Eclipse.
Cấu trúc của luận văn bao gồm: Chương 1 giới thiệu tổng quan về phân tích
chương trình tĩnh. Trong chương này, trình bày định nghĩa kỹ thuật phân tích
chương trình tĩnh, ứng dụng kỹ thuật phân tích, điểm mạnh và những hạn chế của
kỹ thuật phân tích tĩnh. Và phần chính trong Chương 1 là phần kiến thức nền tảng
chính sử dụng trong kỹ thuật phân tích chương trình tĩnh. Tiếp theo là Chương
2 trình bày về phân tích luồng dữ liệu. Cụ thể, trình bày phương pháp phân tích
luồng dữ liệu trong một hàm không có chứa lời gọi hàm (nội thủ tục) và phân tích
luồng dữ liệu đồ thị luồng dữ liệu cho cả chương trình với lời gọi hàm (liên thủ
tục). Chương 3 trình bày phần thực nghiệm với SOOT - một công cụ nguồn mở
để phân tích chương trình viết bằng Java trên môi trường tích hợp phát triển là
Eclipse. Cuối cùng là phần kết luận và các tài liệu tham khảo.
9
Chương 1
Giới thiệu
1.1.
Giới thiệu về phân tích chương trình
Phân tích chương trình tĩnh là kỹ thuật xác định tính chất/hành vi của một
chương trình mà không cần phải chạy chương trình đó. Phân tích tĩnh được xây
dựng dựa trên lý thuyết diễn giải trừu tượng (abstract interpretation) [5, 6] để
chứng minh tính chính xác của các phân tích liên quan đến ngữ nghĩa của một
ngôn ngữ lập trình.
Có rất nhiều câu hỏi thú vị mà có thể được hỏi về một chương trình hoặc các
điểm (point) riêng lẻ trong chương trình như:
• Chương trình có dừng hay không?
• Độ lớn có thể của vùng nhớ (heap) trong khi chạy?
• Đầu ra (output) có thể là gì?
• Biến x có luôn luôn cùng giá trị không?
• Giá trị của x sẽ được đọc trong tương lai?
• Con trỏ p null?
• Biến x đã được khởi tạo trước khi đọc không?
• v.v...
Theo lý thuyết Rice [14], tất cả các câu hỏi trên về hành vi của chương trình là
không thể quyết định/chứng minh được (undecidable).
Thay vì mức mô hình như nhiều phương pháp hình thức, luận văn hướng tới
việc phân tích chương trình tĩnh. Cụ thể, luận văn trình bày một kỹ thuật để cải
10
tiến mã chương trình và phát hiện các lỗi tiềm năng bằng việc phân tích chương
trình tĩnh dựa trên phân tích luồng dữ liệu.
1.2.
Điểm mạnh và điểm yếu
Phân tích chương trình tĩnh có những ưu điểm sau:
• Chỉ ra lỗi tại vị trí chính xác trong chương trình
• Dễ dàng thực hiện bởi những chuyên gia kiểm định chất lượng phần mềm
hiểu rõ về mã nguồn
• Khoảng thời gian ngắn từ lúc phát hiện tới khi sửa lỗi
• Có thể tự động hóa nhanh (thông qua các bộ công cụ hỗ trợ ví dụ: SOOT,
Astree, TVLA,...)
• Lỗi được phát hiện sớm trong qui trình phát triển phần mềm nên chi phí sửa
lỗi thấp.
Tuy nhiên, điểm yếu của kỹ thuật này xuất hiện khi tại một câu lệnh xuất hiện
những tham chiếu, ràng buộc nằm ngoài phạm vi suy luận biểu trưng của chương
trình. Hạn chế này là bản chất của việc phân tích tĩnh - không chạy với dữ liệu cụ
thể. Một số điểm yếu không khắc phục được:
• Mất thời gian nếu phải thực hiện bằng tay
• Việc tự động hóa chỉ hướng vào một ngôn ngữ lập trình (ví dụ: SOOT chỉ
kiểm tra mã nguồn chương trình viết bằng ngôn ngữ Java)
• Thiếu nhân lực có thể hiểu và phân tích được chương trình
• Có thể sinh ra nhiều lời cảnh báo lỗi không chính xác
• Không phát hiện được lỗi chỉ xuất hiện khi chạy chương trình (run-time error).
1.3.
Các công nghệ phân tích chương trình tĩnh
Những kỹ thuật phân tích chương trình tĩnh đã và đang thu hút nhiều nghiên
cứu trên thế giới, hiện có nhiều kỹ thuật nhưng tựu chung có thể phân theo 4 nhóm
chính như sau:
11
Thứ nhất, kỹ thuật phân tích chương trình tĩnh dựa trên phân tích luồng dữ
liệu (data flow analysis) [11, 15]. Phân tích luồng dữ liệu là một quá trình thu
thập thông tin về dữ liệu trong các đoạn mã đó được thực thi trong thực tế trong
chương trình mà không cần phải chạy đoạn mã đó. Tuy nhiên, phân tích luồng dữ
liệu không sử dụng thao tác dựa trên ngữ nghĩa. Phân tích luồng dữ liệu là một
cách rất hiệu quả và khả thi trong việc phát hiện lỗi chương trình và tối ưu hóa
trong các trình biên dịch.
Thứ hai, nhóm kỹ thuật liên quan tới xấp xỉ ngữ nghĩa được gọi là diễn giải
trừu tượng (abstract interpretation) [5, 6]. Kỹ thuật diễn giải trừu tượng dựa trên
nguyên tắc xấp xỉ ngữ nghĩa của chương trình khi kiểm tra đối chiếu sự thỏa mãn
đặc tả. Kỹ thuật này trích ra từ một ngữ nghĩa chuẩn (standard semantics) được một
ngữ nghĩa trừu tượng đã xấp xỉ và tính toán được (approximate and computable
abstract semantics). Quá trình chuyển này không hoàn toàn tự động mà có thể
cần sự tương tác với người dùng. Trong thực tế, kỹ thuật diễn giải trừu tượng có
một thành phần là bộ sinh (generator) ngữ nghĩa trừu tượng đọc mã nguồn chương
trình và tạo ra các ràng buộc hoặc hệ các phương trình cần được giải bởi máy tính
thông qua một thành phần khác là bộ giải (solver). Một phương pháp phổ biến là
dùng hàm lặp khi giải. Việc tìm nghiệm thông qua hàm lặp có hạn chế về mặt thời
gian (phương pháp không hội tụ sau vô hạn lần lặp). Các kỹ thuật liên quan tới
việc tăng tốc hội tụ cũng được nghiên cứu.
Thứ ba, nhóm kỹ thuật liên quan tới mô hình được gọi là kỹ thuật kiểm chứng
mô hình (Model checking) [4]. Mô hình (model) của một hệ thống là một cách
biểu hiện ở mức trừu tượng cao hơn của hệ thống bằng cách lược bỏ những phần
quá chi tiết mà vẫn giữ lại những thông tin cần thiết về hệ thống đang được xem
xét. Trong lĩnh vực phần mềm, kiểm chứng mô hình là cách kiểm tra xem liệu mô
hình của một hệ thống (phần cứng hay phần mềm) thỏa mãn một tính chất nào
đó hay không. Những đặc tả tính chất đó thường là những tính chất an toàn như
khả năng không tồn tại những khóa chết (deadlock) hoặc rơi vào những trạng thái
nguy hiểm tạo sự cố cho hệ thống. . . Nếu một hệ thống không thoả mãn một tính
chất thì kiểm chứng mô hình sẽ đưa ra phản ví dụ với một xâu các trạng thái và sự
kiện liên quan bắt đầu từ trạng thái ban đầu tới trạng thái lỗi của mô hình.
Cuối cùng, kỹ thuật phân tích biểu trưng (symbolic analysis) [18]. Kỹ thuật
này là phân tích tĩnh mã nguồn tĩnh, xây dựng các luồng rẽ nhánh trong chương
trình dựa trên các nút. Tại các nút tương ứng sẽ là tập hợp các ràng buộc (con-
12
straints) của dữ liệu, biến, tham số. Tại nút khởi tạo chương trình, tập hợp các ràng
buộc là rỗng. Càng đi sâu xuống các nhánh nhỏ, tại các nút con, tập hợp ràng buộc
sẽ được tạo ra từ tập hợp ràng buộc tại nút ngay phía trên cộng với điều kiện giữa
các biến số để có thể rẽ từ nút trên vào nút dưới trong luồng chảy chương trình.
Điểm đặc biệt của kỹ thuật này là các tham số hoàn toàn được thể hiện bằng ký
tự biểu trưng, chứ không phải giá trị cụ thể. Ý tưởng của phương pháp này là để
kiểm thử một nhánh trong chương trình, điều kiện tiên quyết là dữ liệu tại đầu vào
phải thỏa mãn tập hợp các ràng buộc tại nút bắt đầu nhánh đó. Việc giải các ràng
buộc gắn với một nút được thực hiện bởi các bộ công cụ sẵn có gọi là giải ràng
buộc (constraint solver) dựa trên SMT (Satisfiability Modulo Theories) hay SAT
(Satisfiability Testing).
Hai nhóm đầu tập trung vào việc nâng cao chất lượng phần mềm tại mức mã
nguồn, trong khi hai nhóm sau xử lý phần mềm tại mức trừu tượng cao hơn – mô
hình. Luận văn sẽ tập trung vào xu thế thứ nhất, đó là kiểu phân tích luồng dữ liệu
dựa trên đồ thị luồng dữ liệu.
1.4.
Nền tảng
1.4.1. Đồ thị luồng điều khiển
Đồ thị luồng điều khiển (Control Flow Graph-CFG) là một đồ thị có hướng,
trong đó các nút (node) tương ứng là các điểm (point) chương trình và các cạnh thể
hiện cho luồng điểu khiển. Một CFG luôn luôn có một điểm của đầu vào, ký hiệu
là entry, và một điểm của đầu ra, ký hiệu là exit. Ngoài ra, nếu v là một nút trong
CFG thì những ký hiệu pred(v) là tập các nút kế trước (predecessor) và succ(v)
là tập các nút kế sau (successor).
CFG cho các lệnh
• Các lệnh cơ bản
Các lệnh đơn giản mà CFG có thể khởi tạo liên quan đến. Những CFG cơ bản trong
ngôn ngữ lập trình Java như là các phép gán (id = E;), output (printf(E);),
lệnh return (return;), và khai báo biến (ví dụ int f;) được môt tả trong Hình 1.1
bên dưới:
13
id = E
printf(E)
return E
int id
Hình 1.1: CFG cho các lệnh cơ bản.
• Các lệnh tuần tự
Cho chuỗi lệnh tuần tự S 1 S 2, ta loại bỏ các nút exit của lệnh S 1 và nút entry của
lệnh S 2 và gắn các lệnh lại với nhau (Hình 1.2).
S1
S1
S2
S2
Hình 1.2: CFG cho các lệnh tuần tự.
• Các lệnh cấu trúc điều khiển
Cấu trúc điều khiển được minh họa bởi đồ thị quy nạp: Các lệnh if, if-else
E
S
if(E) S;
E
S1
S2
if(E) S1; else S2;
Hình 1.3: CFG cho các lệnh if, if-else.
14
Các lệnh while, for
E1
E2
E
S
S
while(E) S;
E3
for(E1; E2; E3;) S;
Hình 1.4: CFG cho các lệnh while, for.
Ví dụ CFG của một chương trình
Sử dụng các cách xây dựng CFG cho từng lệnh ở trên, ta xây dựng CFG cho
một ví dụ chương trình hàm tính giai thừa viết bằng ngôn ngữ Java:
int iterative(int n) {
int f;// khai báo biến (f là kiểu int)
int uu_f;
f = 1;
uu_f = 0;// biến này không là biến sống
while (n > 0){
f = f*n;
n = n - 1;
}
return f;
}
Và được biểu diễn thành CFG như sau:
15
int f
int uu_f
f=1
uu_f = 0
n>0
f = f*n
n=n-1
return f
Hình 1.5: CFG của chương trình tính giai thừa.
1.4.2. Lý thuyết Dàn
Dàn
Trong kỹ thuật phân tích chương trình tĩnh của luận văn, các phân tích sử dụng
cấu trúc toán học là Dàn (Lattices) [16], tập các thuộc tính (ví dụ: tập các biến,
biểu thức,...trong chương trình) cần thiết cho mỗi phân tích tĩnh trong chương
trình.
Định nghĩa Dàn
Một thứ tự bộ phận (partial order) là một cấu trúc toán học: L = (S , ⊑), với S
là một tập và ⊑ là quan hệ hai ngôi trên tập S , thỏa mãn các điều kiện sau:
16
• Phản xạ: ∀x ∈ S : x ⊑ s
• Phản xứng: ∀x, y ∈ S : x ⊑ y ∧ y ⊑ x ⇒ x = y
• Bắc cầu: ∀x, y, z ∈ S : x ⊑ y ∧ y ⊑ z ⇒ x ⊑ z
Biểu diễn Dàn thông qua biểu đồ Hasse
Cho Dàn L = (S , ⊑) là tập có thứ tự bộ phận, biểu đồ Hasse của Dàn L bao
gồm:
• Một tập hợp các điểm trong mặt phẳng tương ứng 1-1 với S, gọi là các đỉnh.
• Một tập hợp các cung nối một số cặp đỉnh có quan hệ thứ tự bộ phận.
Ví dụ, biểu diễn Dàn (2{x,y,x} , ⊆) (Hình 1.6 (a)) hoặc Dàn đảo ngược (Dàn
được sắp bởi thứ tự ngược của các tập con và quan hệ hai ngôi ⊑ được định nghĩa
là ⊇) (2{x,y,x} , ⊇) (Hình 1.6 (b)) bằng biểu đồ Hasse:
{x,y,z}
{}
{x,y}
{x,z}
{y,z}
{x}
{y}
{z}
{x}
{y}
{z}
{x,y}
{x,z}
{y,z}
{}
{x,y,z}
(a)
(b)
Hình 1.6: Biểu đồ Hasse biểu diễn Dàn.
Cận trên, cận dưới
Cho X ⊆ S . Ta nói rằng y ∈ S là một cận trên của X, ký hiệu X ⊑ y, nếu
∀x ∈ X : x ⊑ y. Tương tự, y ∈ S là một cận dưới của X, ký hiệu y ⊑ X, nếu
∀x ∈ X : y ⊑ x. Một cận trên nhỏ nhất, ký hiệu ⊔X, được định nghĩa bởi:
X ⊑ ⊔X ∧ ∀y ∈ X : X ⊑ y ⇒ ⊔X ⊑ y
Bên cạnh đó, một cận dưới lớn nhất, ký hiệu ⊓X, được định nghĩa bởi:
17
⊓X ⊑ X ∧ ∀y ∈ X : y ⊑ X ⇒ y ⊑ ⊓X
Một Dàn là một thứ tự bộ phận trong đó ⊔X và ⊓X tồn tại cho tất cả X ⊆ S .
Phần tử lớn nhất, phân tử nhỏ nhất
Nếu x = ⊔X ∈ X thì x được gọi là phần tử lớn nhất của X, ký hiệu là ⊤ và định
nghĩa là ⊤ = ⊓S . Từ tính phản xạ của quan hệ thứ tự ta suy ra rằng ⊤ nếu tồn tại
là duy nhất.
Tương tự ta có, nếu y = ⊓X ∈ X thì y được gọi là phần tử nhỏ nhất của X, ký
hiệu là ⊥ và định nghĩa là ⊥ = ⊔S . Từ tính phản xạ của quan hệ thứ tự ta suy ra
rằng ⊥ nếu tồn tại là duy nhất.
Do tính duy nhất của các phần tử trong ⊤ và ⊥. Ví dụ minh hoạ dưới đây chỉ ra
những thứ tự bộ phận nào là dàn và không phải là Dàn:
• Những thứ tự bộ phận là Dàn
Hình 1.7: Các biểu đồ Hasse là Dàn.
• Những thứ tự bộ phận không là Dàn
Hình 1.8: Các biểu đồ Hasse không phải là Dàn.
Độ cao của dàn
Độ cao của một Dàn được tính bằng chiều dài từ phần tử nhỏ nhất ⊥ tới phần
tử lớn nhất ⊤. Dàn L = (S , ⊑) là hữu hạn (chiều cao của Dàn là hữu hạn) nếu tập
S chứa hữu hạn số phần tử.
18
Với mỗi tập S hữu hạn định nghĩa một Dàn L = (2S , ⊑), với:
• ⊤, ⊥ tồn tại và ⊥ = ∅, ⊤ = S
• Với mỗi cặp phần tử x, y trong S có x ⊔ y = x ∪ y, x ⊓ y = x ∩ y
Trong ví dụ về Dàn trong Hình 1.6 ở trên thì độ cao của Dàn là 3.
Tổng quát, độ cao của Dàn hữu hạn L = (2S , ⊑) có độ cao là |S |.
Điểm cố định (Fixed-Point)
Hàm đơn điệu
Ánh xạ f : L → L được gọi là hàm đơn điệu khi ∀x, y ∈ S : x ⊑ y ⇒ f (x) ⊑
f (y). Chú ý rằng thuộc tính này không có nghĩa hàm f là hàm tăng (∀x ∈ S : x ⊑
f (x)); Ví dụ, tất cả các hàm hằng là hàm đơn điệu, những hàm ⊔ và ⊓ là những
đơn điệu trong cả hai trường hợp. Lưu ý rằng những phép hợp của những hàm đơn
điệu là hàm đơn điệu.
Điểm cố định
Điều mà ta cần chính là việc tìm ra điểm cố định của một hàm. Theo lý thuyết
điểm cố định [16], trong một Dàn L với độ cao hữu hạn, mọi hàm đơn điệu f có
duy nhất điểm cố định nhỏ nhất được định nghĩa:
⊔
f ix( f ) =
f i (⊥)
i≥0
để có f ( f ix( f )) = f ix( f ). Chứng minh của lý thuyết này khá đơn giản. Chú ý
rằng ⊥⊑ f (⊥) từ đó ⊥ là phần tử nhỏ nhất. Từ đó f là đơn điệu, nó cho phép rằng
f (⊥) ⊑ f 2 (⊥) và bởi phương pháp quy nạp f i (⊥) ⊑ f i+1 (⊥). Do đó, ta có chuỗi
tăng dần:
⊥⊑ f (⊥) ⊑ f 2 (⊥) ⊑ . . .
Vì L được giả thiết là có chiều cao hữu hạn, ta thêm một số k để có f k (⊥) =
f k+1 (⊥). Ta có định nghĩa f ix( f ) = f k (⊥) và vì rằng f ( f ix( f )) = f k+1 (⊥) = f k (⊥
) = f ix( f ), biết rằng f ix( f ) là một điểm cố định. Bây giờ, giả sử rằng x là một
điểm cố định khác. Khi đó ⊥⊑ x ta có f (⊥) ⊑ f (x) = x, vì f là đơn điệu và bằng
quy nạp ta có f ix( f ) = f k (⊥) ⊑ x. Từ đây, f ix( f ) là điểm cố định nhỏ nhất. Theo
tính chất phản xứng, nó cũng là duy nhất.
19
Thuộc tính đóng
Nếu L1 , L2 , ..., Ln là những Dàn với độ cao hữu hạn, từ đó một phép toán tích
(product):
L1 × L2 × ... × Ln = {(x1 , x2 , ..., xn )|xi ∈ L1 }
với ⊑ được định nghĩa là theo từng điểm (point-wise). Với chú ý rằng ⊔ và ⊓
có thể được tính toán theo từng điểm và như vậy height(L1 × L2 × ... × Ln ) =
height(L1 ) + ... + height(Ln ).
Tương tự ta có, một phép toán cộng (sum):
L1 + L2 + ... + Ln = {(i, xi )|xi ∈ Li \ {⊥, ⊤}} ∪ {⊥, ⊤}
với ⊤ và ⊥ được cho trước và (i, x) ⊑ ( j, y) khi và chỉ khi i = j và x ⊑ y. Chú ý
rằng height (L1 + ... + Ln ) = max{height(Li )}. Phép toán cộng được minh họa như
sau:
Hình 1.9: Phép toán cộng dàn.
Nếu Dàn L là một Dàn với độ cao hữu hạn, khi đó li f t(L), độ cao của Dàn L
là: height(li f t(L)) = height(L) + 1, minh họa như sau:
Hình 1.10: Phép toán nâng (lift) dàn.
20
Nếu A là một tập hữu hạn (A không cần thiết phải là một Dàn), khi đó f lat(A)
được minh họa bởi:
Hình 1.11: Phép toán lift của các tập tạo thành dàn.
Và f lat(A) là một Dàn có độ cao là 2.
Cuối cùng, nếu A và L được định nghĩa như trên, khi đó chúng ta thu được một
Dàn ánh xạ (map) với độ cao như sau:
A 7→ L = {[a1 x1 , ..., an 7→ xn ]|xi ∈ L}
theo từng điểm thứ tự: f ⊑ g ⇔ ∀ai : f (ai ) ⊑ g(ai ). Nếu A là hữu hạn và L có độ
cao hữu hạn khi đó height(A 7→ L) = |A|.height(L).
Phương trình và bất phương trình
Cho L là một Dàn với độ cao hữu hạn. Một hệ phương trình được biểu diễn:
x1 = F1 (x1 , ..., xn )
x2 = F2 (x1 , ..., xn )
...
xn = Fn (x1 , ..., xn )
với xi là những biến và Fi : Ln → L là một tập những hàm đơn điệu. Mỗi hệ
chỉ có nghiệm nhỏ nhất duy nhất, nó được gọi là điểm cố định nhỏ nhất của hàm
F : Ln → L được định nghĩa bởi:
F(x1 , x2 , ..., xn ) = (F1 (x1 , x2 , ..., xn ), ..., Fn (x1 , x2 , ..., xn ))
- Xem thêm -