ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ

NGUYỄN MINH HẢI

PHÁT TRIỂN CÁC KỸ THUẬT TÌM BẤT BIẾN
(INVARIANTS) VÀ BIẾN (VARIANTS) CHO VIỆC
SỬ DỤNG HOARE LOGIC ĐỂ CHỨNG MINH TÍNH
ĐÚNG ĐẮN CỦA CHU TRÌNH

LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN

Hà Nội – 2016


ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ

NGUYỄN MINH HẢI

PHÁT TRIỂN CÁC KỸ THUẬT TÌM BẤT BIẾN
(INVARIANTS) VÀ BIẾN (VARIANTS) CHO VIỆC
SỬ DỤNG HOARE LOGIC ĐỂ CHỨNG MINH TÍNH
ĐÚNG ĐẮN CỦA CHU TRÌNH

Ngành: Công nghệ Thông tin
Chuyên ngành: Kỹ thuật phần mềm
Mã số: 60480103

LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN
NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. ĐẶNG VĂN HƯNG

1


LỜI CAM ĐOAN
Tôi xin cam đoan luận văn “Phát triển các kỹ thuật tìm bất biến (invariants)
và biến (variants) cho việc sử dụng Hoare Logic để chứng minh tính đúng đắn của
chu trình” là do tôi thực hiện, được hoàn thành trên cơ sở tìm kiếm, thu thập,
nghiên cứu, tổng hợp phần lý thuyết và các phương pháp kĩ thuật được trình bày
trong các tài liệu được công bố trong nước và trên thế giới. Các tài liệu tham khảo
đều được nêu ở phần cuối của luận văn. Luận văn này không sao chép nguyên bản
từ bất kì một nguồn tài liệu nào khác.
Nếu có gì sai sót, tôi xin chịu mọi trách nhiệm.

Hà Nội, tháng 11 năm 2016
Tác giả luận văn

Nguyễn Minh Hải

2


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 HÌNH VẼ ............................................................................ 5
CHƯƠNG 1. MỞ ĐẦU...................................................................................... 6
LÝ DO CHỌN ĐỀ TÀI ................................................................................................. 6
MỤC ĐÍCH NGHIÊN CỨU ........................................................................................... 6
ĐỐI TƯỢNG VÀ PHẠM VI NGHIÊN CỨU ..................................................................... 7

4.3.1 Tìm phần tử có giá trị lớn nhất trong một dãy các phần tử ................... 32
4.3.1.1 Số lớn nhất với vòng lặp một biến ...................................................... 32
4.3.1.2 Số lớn nhất với vòng lặp hai biến ....................................................... 33
4.3.2 Tìm kiếm ................................................................................................... 35
4.3.2.1 Tìm kiếm trong một mảng chưa được sắp xếp .................................. 35
4.3.2.2 Tìm kiếm nhị phân.............................................................................. 36
4.3.3 Sắp xếp ...................................................................................................... 39
4.4 ỨNG DỤNG KINH NGHIỆM ĐỂ TÌM BIẾN, BẤT BIẾN TRONG MỘT SỐ BÀI TOÁN. . 42

CHƯƠNG 5. KẾT LUẬN ................................................................................ 61
5.1 KẾT LUẬN......................................................................................................... 61
5.2 HẠN CHẾ VÀ KIẾN NGHỊ ................................................................................... 61

TÀI LIỆU THAM KHẢO ................................................................................ 63

4


DANH MỤC CÁC HÌNH VẼ
Hình 2. 1. Ảnh Tony Hoare và Robert Floyd ………………………………………12
Hình 4. 1 . Các vòng lặp như là một sự tính toán bằng cách xấp xỉ .................. 27
Hình 4. 2. Ước số chung lớn nhất của hai số nguyên dương a và b .................. 29
Hình 4. 3. Số lớn nhất với vòng lặp một biến .................................................... 33
Hình 4. 4. Số lớn nhất với vòng lặp hai biến. .................................................... 34
Hình 4.5. Tìm kiếm trong một mảng chưa được sắp xếp. .................................. 36
Hình 4. 6. Tìm kiếm nhị phân ........................................................................... 39
Hình 4. 7. Sắp xếp kiểu nổi bọt. ........................................................................ 41

5


Hoare. Bên cạnh đó, việc đưa ra những gợi mở về bản chất của vòng lặp thông
qua bất biến vòng lặp được trú trọng. Các chương trong luận văn sẽ cung cấp cái
nhìn tổng quan nhất về biến và bất biến bằng những lý thuyết và bài toán áp dụng
trên các thuật toán cơ bản. Phát triển các kỹ thuật tìm bất biến (invariants) và biến
(variants) cho việc sử dụng logic Hoare để chứng minh tính đúng đắn của chu
trình là mục đích nghiên cứu chủ yếu của luận văn.
6


Việc hiểu, làm rõ các vấn đề liên quan đến tính đúng của chu trình, bản chất
của vòng lặp, tính kết thúc… sẽ là những cơ sở quan trọng cho công việc dạy học
THPT của bản thân tôi và các bạn đồng nghiệp khác.
Đối tượng và phạm vi nghiên cứu
Đối tượng và phạm vi nghiên cứu của luận văn xoay quanh logic Hoare.
Nó bao gồm những kiến thức cơ bản của luận lý đó là bộ ba Hoare, các tiên để
của luận lý. Luận văn cũng nêu rõ những đặc điểm nổi bật và áp dụng vào việc
chứng minh tính đúng đắn của chương trình mà cơ bản tập trung vào việc chứng
minh tính đúng đắn của lệnh chu trình. Thông qua các bài toán cơ bản, tôi thực tế
áp dụng lý thuyết của logic Hoare vào việc chứng minh này.
Nghiên cứu tập chung vào tìm biến và bất biến. Áp dụng trên các thuật toán
cơ bản trong chương trình tin học.
Kết cấu của luận văn
Gồm có 5 chương:
Chương 1. Mở đầu. Giới thiệu lý do chọn đề tài, mục đích nghiên cứu, đối
tượng và phạm vi nghiên cứu, kết cấu của luận văn.
Chương 2. Tổng quan về logic Hoare. Chương này cung cấp cho tôi những
lý thuyết cơ bản về logic vị từ và logic Hoare.
Chương 3. Chứng minh tính đúng đắn của lệnh chu trình bằng logic Hoare.
Trong chương cung cấp những cách thức cơ bản để chứng minh tính đúng đắn.
Bên cạnh đó, tôi áp dụng thực tế các lý thuyết vào việc chứng minh trong một vài

r:=0; s:= -1; x:= 0;
While r ≤ y do
Begin
s:= s + 2;
r:= r + s;
x := x + 1;
End
Tìm biết ( t ) và bất biến ( I ) để chứng minh tính đúng đắn của lệnh chu trình.
Giải: Dự đoán biến và bất biến
Biến
Nhận thấy biến chỉ số r tăng tuần tự và là bình phương của x. Vòng lặp sẽ
kết thúc khi r vượt quá n. Đối với dạng điều kiện lặp có một biến chỉ số (r), theo
kinh nghiệm tôi đưa ra một biến chức năng t = n – r + 1. Ở đầu ra của vòng lặp
biến chức năng sẽ có giá trị t ≤ 0.
Bất biến
Phân tích qua đoạn chương trình tôi nhận thấy nó dùng để trả ra phần
nguyên căn bậc hai của một số nguyên dương y ([√y] = x -1). Các biến trong thân
vòng lặp có giá trị s = 2x - 1, r  x 2 . Tôi dự đoán một bất biến vòng lặp từ những
dữ liệu vừa phân tích I  r  x 2  s  2 x  1   x  1  y
2

Chứng minh biến và bất biến vừa tìm được là đúng.
Biến
59


Xem lại chứng minh ở bài 2, 4, 5, 6.
Bất biến
Tôi chứng minh b  I  c I  . Áp dụng vào thân vòng lặp tôi có



I

Có r  s  2   x  1  s  2  2 x  1  x 2  y 
2

r  x2  s  2 x  1  x2  y .
Khi đó tôi cần phải chỉ ra r  x 2  s  2 x  1   x  1  y  r  y 
2

r  x2  s  2 x  1  x 2  y . Điều đó được minh chứng bằng những logic sau:
r  x2
s  2x  1
ry

Theo giả thiết
Theo giả thiết
Theo giả thiết

x2  y

Vì r  x 2 .

Kết luận : Bất biến và biến tôi dự đoán là đúng.
Như vậy, tôi nhận thấy vấn đề tìm biến và bất biến để chứng minh tính đúng
đắn của lệnh chu trình thực sự không thể tìm được một phương pháp chung nhất,
hay phương pháp đảm bảo tối ưu. Vì cơ bản những bài toán khác nhau đều có hậu
điều kiện và các ràng buộc khác nhau, điều đó mang lại sự đa dạng bất quy tắc.
Để giải quyết được bài toán này chủ yếu dựa vào các giải pháp được đúc rút ra
dựa trên những kinh nghiệm được học hỏi và khám phá trong quá trình tìm tòi.