Header Page 1 of 113.
ĐẠ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

Footer Page 1 of 113.


Header Page 2 of 113.
ĐẠ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

đào tạo tỉnh Lạng Sơn đã tạo điều kiện cho tôi có được cơ hội học tập, nâng cao
trình độ chuyên môn.
Cuối cùng, lời cảm ơn chân thành của tôi xin gửi đến các bạn học cùng lớp
K21 Công nghệ phần mềm đã thường xuyên quan tâm, giúp đỡ, chia sẻ kinh
nghiệm, tài liệu hữu ích trong suốt quá trình học tập.
Một lần nữa, tôi xin cảm ơn và gửi lời chúc sức khỏe, thành công đến tất cả
mọi người.

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

Nguyễn Minh Hải

Footer Page 4 of 113.

1


Header Page 5 of 113.

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.


CHƯƠNG 3. CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH
BẰNG LOGIC HOARE ................................................................................... 15
3.1 PHƯƠNG PHÁP CHỨNG MINH............................................................................ 15
3.2 CÁC VÍ DỤ ÁP DỤNG.......................................................................................... 17

CHƯƠNG 4. NGHIÊN CỨU VỀ BIẾN VÀ BẤT BIẾN TRONG PHƯƠNG
PHÁP CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH .......... 24
4.1 BIẾN ................................................................................................................. 24
4.1.1 Khái niệm .................................................................................................. 24
4.1.2 Phương pháp tìm biến .............................................................................. 24
4.2 BẤT BIẾN .......................................................................................................... 25
4.2.1 Bất biến vòng lặp ...................................................................................... 25
4.2.2 Một cách nhìn mang tính xây dựng ......................................................... 27
4.2.3 Ví dụ cơ bản .............................................................................................. 28
4.2.4 Phân loại bất biến: .................................................................................... 30
4.2.4.1 Phân loại theo luật .............................................................................. 30
4.2.4.2 Phân loại theo kỹ thuật khái quát hóa ............................................... 31
4.3 TÌM BIẾN VÀ BẤT BIẾN VÒNG LẶP TRONG MỘT VÀI THUẬT TOÁN CƠ BẢN....... 32

Footer Page 6 of 113.

3


Header Page 7 of 113.
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



Header Page 9 of 113.

CHƯƠNG 1. MỞ ĐẦU
Lý do chọn đề tài
Trong suốt quá trình tôi được học tập, nghiên cứu tại trường Đại học Công
nghệ, Đại học Quốc Gia Hà Nội. Bản thân đã được tiếp xúc với nhiều kiến thức
mới, quan trọng, được ứng dụng mạnh mẽ trong các lĩnh vực rộng lớn của CNTT.
Là một giáo viên giảng dạy bộ môn tin học tại cấp THPT, tôi thường xuyên tiếp
xúc và hướng dẫn học sinh những kiến thức cơ bản về ngôn ngữ lập trình trên cơ
sở là ngôn ngữ Pascal. Do đó, tôi đặc biệt có hứng thú với bộ môn kiểm thử. Việc
kiểm tra một chương trình xem nó có đúng, chạy tốt, phù hợp với yêu cầu của
người lập trình hay không luôn là một vấn đề quan trọng, mang tính thời đại đối
với mọi lập trình viên cũng như các nhà quản lý phần mềm. Cả dự án có thể bị
ảnh hưởng nếu gặp những lỗi nghiêm trọng trong việc viết mã. Trong những tính
chất đảm bảo chương trình phù hợp với yêu cầu, có một tính chất rất quan trọng
đó là tính đúng đắn.
Việc chứng mình một chương trình là đúng đắn có nhiều phương pháp,
trong phần nghiên cứu của luận văn, tôi chọn nghiên cứu Hoare logic (logic
Hoare). Logic Hoare được Hoare xuất bản trong một bài báo năm 1969. Nó thực
sự đã được ra đời rất lâu, nhưng bản thân nó luôn mang tính thời đại vì việc áp
dụng logic Hoare để kiểm tra tính đúng của chương trình vẫn đang được tiến hành
thường xuyên trên phạm vi rộng lớn. Việc tìm hiểu về phương pháp chứng minh
tính đúng logic Hoare đã gợi mở cho tôi một hướng nghiên cứu. Trong đó, tôi đi
xâu vào việc phân tích về Biến (Variants) và Bất biến (Invariants), hai yếu tố quan
trọng đầu tiên trong việc chứng minh tính đúng của lệnh chu trình. Bản chất của
một vòng lặp luôn có sự ẩn chứa của một bất biến vòng lặp. Hay nói cách khác,
bạn không thể hiểu được vòng lặp nếu chưa biết về bất biến của nó.
Mục đích nghiên cứu

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
bài toán cơ bản.
Chương 4. Nghiên cứu về biến và bất biến trong phương pháp chứng minh
tính đúng đắn của lệnh chu trình. Ứng dụng vào tìm biến và bất biến trong một số
thuật toán cơ bản.
Chương 5. Kết luận. Chương tổng kết lại những vấn đề đạt được, chưa đạt
được và những kiến nghị đề xuất của luận văn.

Footer Page 10 of 113.

7


Header Page 11 of 113.

CHƯƠNG 2. TỔNG QUAN VỀ LOGIC HOARE
2.1. Logic vị từ
 Định nghĩa: Vị từ là một hàm nhận một giá trị kiểu boolean
Một vị từ thực sự là một giá trị logic được biểu hiện bằng tham số. Nó có
thể đúng với một số đối số, và sai với một số đối số khác. Chẳng hạn x  0 là một
vị từ với một đối số, tôi có thể đặt tên đó là gt (x) . Do vậy mà gt (5) tức là 5  0
là đúng và gt (0) tức là 0  0 là sai.
Cụ thể hơn tôi phân tích một phát biểu “x bằng 3” nhận thấy nó có hai bộ
phận. Bộ phận thứ nhất là biến x, là chủ ngữ của câu. Bộ phận thứ hai “bằng 3” là

với mọi x, và lượng hóa tồn tại, x đọc là tồn tại x. Trong sơ đồ ưu tiên để tránh
các dấu ngoặc trong các công thức,  có độ ưu tiên thấp nhất trong các liên kết.
Ví dụ:
 Với lượng từ “với mọi x ( x ) ”. Diễn đạt câu: “Tất cả học sinh đều
mang máy tính đến trường”. Giải: Cho P  x  là ký hiệu của câu “
mang máy tính đến trường ”. Khi đó câu “Tất cả học sinh đều mang
máy tính đến trường” được viết là x.P  x  , ở đây không gian gồm
tất cả học sinh.
 Với lượng từ “Tồn tại x( x )”. Diễn đạt câu: “Có ít nhất một học sinh
mang máy tính đến trường”. Giải: Cho P  x  là ký hiệu của câu “
mang máy tính đến trường ”. Khi đó câu “Có ít nhất một học sinh
mang máy tính đến trường” được viết là x.P  x  , ở đây không gian
là ít nhất một học sinh.
 Một công thức đúng ngữ pháp của logic vị từ được định nghĩa đệ quy như
sau:
o Mỗi công thức nguyên tử là một công thức đúng ngữ pháp wff, và
o Nếu  và  là wffs và x là một tên biến, thì mỗi công thức sau đây
cũng là một công thức đúng ngữ pháp:
 ( )
 (   )
 (   )
 (   )
 (x. )
 (x. )
 (   )
Hai phép toán lượng hóa cung cấp một ngữ nghĩa không thể thiếu được để
biển diễn các khảng định về các kết quả chân lý của các vị từ. Sự thể hiện của mỗi
phép toán trong các phép toán logic phụ thuộc vào hiểu biết về không gian từ đó
các giá trị của các biến có thể được đưa ra. Nếu không gian này là hữu hạn, nói
rằng c1,c2 ...,ck  , thì những phép toán logic mới này có thể được hiện thị bằng

o Một phép gán 
 Mỗi tên vị từ n đối số thành một quan hệ n vị trí trong D
 Mỗi tên hàm n đối số thành một hàm n vị trí trong D
 Mỗi định danh hằng thành một phần tử của D
Tôi viết i   D,  
Một thể hiện là một toán hạng thể hiện nếu D là tất cả các toán hạng, và các
phép gán đối với mỗi tên hàm là toán hạng khởi tạo tương ứng,

  f   t1,..., tk   f t1,..., tk  .
 Một thể hiện được cho i   D,   , một biến gán (hoặc trạng thái)  là hàm
cho tập các biến V ,  : V  D . Phép gán được mở rộng một cách đệ quy để mang
một giá trị cho tất cả các toán hạng và các công thức:

Footer Page 13 of 113.

10


Header Page 14 of 113.
o Đối với các toán hạng:
 Với biến x, val  x     x , và đối với hằng c, val  c     c 


Với

một

toán

hạng

 Một công thức đúng ngữ pháp wff là hệ quả logic của một tập các công
thức đúng ngữ pháp ,  |  nếu mội thể hiện và trạng thái thỏa mãn mỗi   ,
 và  là tương đương logic,

   nếu với mọi thể hiện và trạng thái  ,

val    val   
2.2. Những hiểu biết về Logic Hoare
2.2.1 Lịch sử của logic Hoare:
Logic Hoare (còn được biết đến với cái tên logic Floyd-Hoare) là một hệ
chính quy do nhà khoa học máy tính người Anh C.A.R Hoare phát triển, và sau
đó được Hoare và những nhà nghiên cứu khác tinh lọc lại. Mục đích của hệ thống
là cung cấp một tập các quy luật luận lý để suy luận tính đúng đắn của chương

Footer Page 14 of 113.

11


Header Page 15 of 113.
trình máy tính bằng tính chính xác của luận lý toán học. Nó được xuất bản trong
bài báo của Hoare vào năm 1969, ở đó Hoare đã sử dụng lại những đóng góp trước
đó của Robert Floyd, người đã xuất bản một hệ thống nghiên cứu tương tự đối với
sơ đồ luồng(flowchart).

Tony Hoare

Robert Floyd

Hình 2. 2. Ảnh Tony Hoare và Robert Floyd

Tôi giả thiết rằng x : E biểu thị một lệnh gán, trong đó x là một biến và E
là một biểu thức thích hợp, P là một công thức logic vị từ. Khi đó, luật về phép
gán được phát biểu như sau P  x / E  x:=E P

P  x / E  chỉ ra rằng biểu thức P trong đó tất cả các lần xuất hiện tự do của
biến x đã được thay bằng biểu thức E. Ý nghĩa là giá trị đúng hay sai của P  x / E 
tương đương với giá trị đúng hay sai của P sau khi gán. Cụ thể hơn, nếu

P  x / E  là true trước phép gán, nhờ tiên đề gán P sẽ là true sau phép gán.
Ngược lại, nếu P  x / E  là false trước phép gán, nhờ tiên đề gán P sẽ là false
sau phép gán.
Xét ví dụ:  y  1  33 x:=y+1  x  33 , tôi thấy  y  1  33 là đúng, qua
phép gán x:=y+1 dễ dàng nhận thấy x có giá trị là 33. Vậy bộ ba Hoare ở trên là
đúng.
Các quy tắc bổ trợ :
Độ mạnh của các công thức đúng ngữ pháp:
Nếu P và Q là hai công thức đúng ngữ pháp, mà P  P ' thì khi đó tôi nói
P là công thức mạnh hơn P’ và P’ thì yếu hơn P. Một điều kiện mạnh hơn là một
điều kiện mà có ít các giá trị thỏa mãn nó hơn điều kiện kia.
Độ mạnh của điều kiện trước:
Đó là quy tắc đầu tiên của các quy tắc suy luận trong hệ chứng minh chương
trình. Ý kiến một cách trực quan là nếu một xác nhận chương trình có thể được
chứng minh, thì điều kiện trước có thể được thay thế bởi bất kỳ công thức nào kéo
theo nó.

P ' c 'Q ,P  P'
P c 'Q
c là một đoạn chương trình bất kỳ.
Độ yếu của điều kiện sau:
Đó là quy tắc tiếp theo của quy tắc suy luận trong hệ thống chứng minh

Luật While dành cho tính đúng đắn toàn phần

P  B  t  N  C P  t  N  P  t  0
P while B do C B  P
Luật này dùng để chứng minh tính đúng đắn toàn phần của lệnh chu trình.
Trong luật này, ngoài việc giữ các điều kiện của bất biến vòng lặp tôi còn phải
chứng minh tính dừng bằng cách chứng minh giá trị của một số hạng (t) giảm dần
sau mỗi lần lặp. t được gọi là biến, chú ý rằng t phải thuộc tập chắc chắn, để cho
mỗi lần lặp có thể giảm đi một giá trị hữu hạn nào đó.
Trong phần đề tài này, tôi sẽ chỉ tập trung vào việc chứng minh tính đứng
đắn toàn phần của lệnh chu trình bằng logic Hoare. Trên cơ sở lập trình, bản chất
của mỗi chương trình gồm nhiều yếu tố, trong đó lệnh chu trình luôn là vấn đề
căn bản hay còn gọi là lõi của chương trình. Người lập trình và người kiểm thử
tính đúng đắn của chương trình luôn phải giành nhiều thời gian tập trung vào nó.
Việc sử dụng luật While dành cho tính đúng đắn toàn phần của lệnh chu trình sẽ
được tìm hiểu sâu và áp dụng trong các chương sau.

Footer Page 17 of 113.

14


Header Page 18 of 113.

CHƯƠNG 3. CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH
CHU TRÌNH BẰNG LOGIC HOARE
3.1 Phương pháp chứng minh
Như tôi đã biết mục tiêu của logic Hoare là để cung cấp một hệ thống chính
thức cho lý luận về tính đúng đắn của chương trình bằng lý thuyết logic toán học.
Logic Hoare được dựa trên ý tưởng được đặc tả như một hợp đồng giữa việc thực


15


Header Page 19 of 113.
wp (S, T, Q) = wp (S, wp (T, Q))
wp (if B then S else T, Q) = B ⇒ wp (S, Q) && ¬B ⇒ wp (T, Q)
Để xác minh tính chính xác một phần của các vòng lặp có dạng hình thức
while b do c, tôi cần một bất biến I sao cho các điều kiện sau đây được thỏa mãn:
 P  I : Các bất biến bước đầu là đúng.


I  b c I  : Mỗi lần thực hiện vòng lặp luôn bảo tồn bất biến, tức là sau
mỗi lần thực hiện thân vòng lặp thể hiện bất biến luôn được giữ nguyên.



 I  b   Q : Các bất biến và điều kiện thoát vòng lặp bao hàm hậu điều
kiện.

Tôi có thể xác minh đầy đủ tính đúng đắn của vòng lặp bằng cách đưa ra
một biến chức năng có giá trị nguyên t, đáp ứng các điều kiện sau đây:
 I  b  t  0 : Nếu tôi đi vào thân vòng lặp (nghĩa là điều kiện lặp b được
đánh giá đúng) và bất biến được bảo tồn, sau đó t phải được khảng định
đúng. Tôi thấy t  0 nghĩa là biến chức năng có giá trị dương, điều đó cần
được đảm bảo để có thể bắt đầu thân vòng lăp.


I  b  t  N c t  N : Giá trị của biến chức năng sẽ giảm sau mỗi lần


Trên thực tế, với hàng tỉ bài toán khác nhau, có những đặc điểm vô tận
trong việc dùng vòng lặp có dạng thức while b do c để thể hiện. Để rèn luyện và
làm rõ cách thức chứng minh tính đúng đắn dựa trên lý thuyết của Hoare, tôi sẽ
lần lượt làm các ví dụ. Trong phần này, tôi sẽ thực hiện hai ví dụ sau đây:
Ví dụ 1. Tính tổng từ 1..n
n


i  1  s  0 while i  n do (s : s  i;i : i  1) s   j 
j 1 


Giải:
Để chứng minh tính đúng của lệnh lặp tôi cần xác định một bất biến vòng
lặp I từ dữ liệu của đoạn lệnh. Ở bài này, bất biến lặp sẽ được tìm bằng cách thay
n


đổi các giá trị hậu điều kiện Q   s   j  để sao cho nó phụ thuộc vào chỉ số
j 1 

của vòng lặp, ở đây là i. Tôi nhận thấy i chạy từ 1 tiến dần đến n+1, đó là
1  i  n  1 , khi i = n+1 vòng lặp sẽ thoát. Do đó, tôi sẽ thay n bằng i:

i

I  s   j . Đương nhiên, tôi dễ dàng xác định được giá trị nhỏ nhất của tổng
j 1

s là bằng 0 khi i=1. Điều này làm tôi sẽ phải thay đổi một chút trong bất biến vòng


 I  i  n  s   j
j 1

Đầu tiên, tôi cần đảm bảo bất biến là đúng khi thực hiện vòng lặp. việc đó
đúng khi tôi chứng minh được  i  1  s  0   I . Để thực hiện, tôi cần truyền
vào bất biến vòng lặp I (áp dụng luật phép gán và tuần tự) giá trị điều kiện ban
đầu như sau:
11

i=1 tôi có 1  1  n  1  s   j
j 1

11

s=0 tôi có 0   j
j 1

Tới đây, nhiệm vụ của tôi là cần phải cho thấy rằng:
11

i  1  s  0  1  1  n  1  0   j Bằng các logic dưới đây
j 1

11

1 n 1
nhiên có 1  n  1.

Đúng với logic toán học.


logic toán học

Footer Page 21 of 113.

18


Header Page 22 of 113.
Tiếp theo là việc chứng minh sau mỗi lần lặp bất biến vòng lặp không đổi
và sau đó tôi còn phải khảng định tính dừng bằng cách chứng minh giá trị của
biến t giảm dần sau mỗi lần lặp. Điều đó được thực hiện khi tôi chứng minh vấn
đề sau là đúng:
i 1


1  i  n  1  s   j  i  n  n  i  1  N 
j 1



I bt  N

( i 1) 1


1

i


ghép

s : s  i
( i 1) 1


1  i  1  n  1  s   j  n  (i  1)  1  N 
j 1


i : i  1

Luật phép gán

i 1


1

i

n

1

s

j  n  i 1 N 




j 1

1 i 1
in
i 1  n 1

Bởi gì 1  i
Theo giả thiết
Cộng 2 vế thêm 1

i 1

s   j  1  ...  (i  1)

Theo giả thiết

j 1

si 

i 11

 j  1  ...  (i  1)  i

cộng 2 vế thêm i

j 1

Vấn đề thứ hai là chứng minh giá trị của t giảm dần: Sau khi thực hiện lặp


n

1

s

j

i

n

s

j




j

1
j

1


Theo giả thiết
in



Bài 2. Tính r  nm

r : 1; i : 0 while i  m do  r : r * n; i : i  1 r  nm
Giải:
Để có những căn cứ đầu tiên xác định các thành phần trong việc chứng
minh tính đúng đắn của lệnh chu trình trên đây, tôi cần xác định các điều kiện tiên
quyết thích hợp với bài toán. Tôi nhận thấy biến chỉ số i của lệnh lặp chạy trong
miền giá trị từ 0 đến m do đó điều kiện đầu tiên có được là 0  i  m . Để tránh
tình trạng có vấn đề trong trường hợp 00 tôi giả sử n  0 và m  0 . Như vậy,
những điều kiện đầu tiên có được đó là 0  i  m  n  0 .
Công việc tiếp theo luôn là xác định một bất biến vòng lặp chuẩn xác. Nó
thực sự là vấn đề quan trọng trong việc có những tiền đề để chứng minh tính đúng
đắn của lệnh chu trình. Bất biến vòng lặp I, cũng như trong bài toán 1 ở trên, tôi
thay đổi hậu điều kiện r  nm  để cho nó phụ thuộc vào chỉ số vòng lặp thay vì

một số biến khác nào đó. Tôi thử thay thế m  i do đó r  ni là lựa chọn đầu tiên
cho bất biến vòng lặp. Tuy nhiên r  ni chưa phải là một bất biến vòng lặp đầy

Footer Page 23 of 113.

20


Header Page 24 of 113.
đủ. Bởi vì: đầu tiên nó luôn phải đi liền với các điều kiện thoát khỏi vòng lặp để
có được hậu điều kiện. Ở đây điều kiện thoát vòng lặp là i  m . Tôi cần chú ý
rằng thực ra khi đó i chỉ có giá trị đến m. Sau đó, để chứng minh các cơ chế lặp
đúng tôi cần thêm các điều kiện 0  i  m  n  0 vào bất biến vòng lặp. Cuối


0m

Đúng theo giả thiết

n0

Đúng theo giả thiết

1  n0

Đúng với mọi n  0

Footer Page 24 of 113.

21


Header Page 25 of 113.
Chứng minh biến chức năng t ban đầu là dương, bởi sau khi thực hiện vòng
lặp nó sẽ giảm dần và khi bằng 0 vòng lặp phải được dừng và thoát.

0  i  m  n  0  r  ni  i  m  m  i  0 Tôi sẽ chứng minh như sau:
im

Theo giả thiết

mi  0

Trừ i ở cả hai vế của bất đẳng thức


Luật phép gán

I t  N

Đầu tiên là việc chứng minh bất biến vòng lặp I không đổi sau khi thực
hiện phần thân của lệnh lặp. khi đó, nghĩa vụ của tôi là phải chứng minh

0  i  m  n  0  r  ni  i  m  0  i  1  m  n  0  r * n  ni1 là đúng
bằng các logic sau:
0  i 1
im

i 1  m 1

Bởi vì 0  i
Theo giả thiết
Cộng thêm 1 vào hai vế của bất phương

trình.
i 1  m

n0

Theo định nghĩa 
Theo giả thiết

r  ni

Giả thiết