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

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

1

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

Hà Nội - 2016

2

1

LỜI CẢM ƠN

Trước tiên, tôi xin chân thành cảm ơn TS. Đặng Văn Hưng, người thầy đã

tận tình hướng dẫn, giúp đỡ tôi trong suốt quá trình học tập và thời gian hoàn

thành luận văn tốt nghiệp.

Tôi cũng xin chân thành cảm ơn các thầy cô giáo khoa Công nghệ thông

tin, Trường đại học công nghệ, Đại học quốc gia hà nội, những người đã hết mình,

tận tụy truyền đạt kiến thức, đã quan tâm, động viên trong suốt quá trình tôi học

tập và nghiên cứu tại Trường.

Tôi xin gửi lời cảm ơn đến đơn vị Trường THPT Bình gia, Sở giáo dục và

đà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

2

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

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

KẾT CẤU CỦA LUẬN VĂN..........................................................................................7

CHƯƠNG 2. TỔNG QUAN VỀ LOGIC HOARE............................................. 8

2.1. LOGIC VỊ TỪ......................................................................................................8

2.2. NHỮNG HIỂU BIẾT VỀ LOGIC HOARE .............................................................11

2.2.1 Lịch sử của logic Hoare:...........................................................................11

2.2.2. Nội dung của logic Hoare ........................................................................12

2.2.3. Các tiên đề của logic Hoare:....................................................................12

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