Tóm tắt Luận văn Thạc sĩ Công nghệ thông tin: 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<br /> TRƯỜNG ĐẠI HỌC CÔNG NGHỆ<br /> <br /> NGUYỄN MINH HẢI<br /> <br /> PHÁT TRIỂN CÁC KỸ THUẬT TÌM BẤT BIẾN (INVARIANTS)<br /> VÀ BIẾN (VARIANTS) CHO VIỆC SỬ DỤNG HOARE LOGIC ĐỂ<br /> CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA CHU TRÌNH<br /> <br /> Ngành: Công nghệ Thông tin<br /> Chuyên ngành: Kỹ thuật phần mềm<br /> Mã số: 60480103<br /> TÓM TẮT LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN<br /> <br /> NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. ĐẶNG VĂN HƯNG<br /> <br /> Hà Nội - 2016<br /> <br /> i<br /> <br /> MỤC LỤC<br /> MỤC LỤC ........................................................................................................ II<br /> DANH MỤC CÁC HÌNH VẼ ......................................................................... III<br /> CHƯƠNG 1. MỞ ĐẦU ..................................................................................... 1<br /> LÝ DO CHỌN ĐỀ TÀI ...................................................................................... 1<br /> MỤC ĐÍCH NGHIÊN CỨU ............................................................................... 1<br /> ĐỐI TƯỢNG VÀ PHẠM VI NGHIÊN CỨU ......................................................... 1<br /> KẾT CẤU CỦA LUẬN VĂN .............................................................................. 1<br /> CHƯƠNG 2. TỔNG QUAN VỀ LOGIC HOARE ........................................... 2<br /> 2.1. LOGIC VỊ TỪ ........................................................................................... 2<br /> 2.2. NHỮNG HIỂU BIẾT VỀ LOGIC HOARE ................................................... 2<br /> 2.2.1 Lịch sử của logic Hoare: ................................................................. 2<br /> 2.2.2. Nội dung của logic Hoare .............................................................. 2<br /> 2.2.3. Các tiên đề của logic Hoare:.......................................................... 2<br /> CHƯƠNG 3. CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH<br /> BẰNG LOGIC HOARE .................................................................................... 4<br /> 3.1 PHƯƠNG PHÁP CHỨNG MINH.................................................................. 4<br /> 3.2 CÁC VÍ DỤ CHỨNG MINH :....................................................................... 5<br /> 3.2.1 Bài 1 .................................................................................................. 5<br /> 3.2.2 Bài 2 .................................................................................................. 6<br /> CHƯƠNG 4. NGHIÊN CỨU VỀ BIẾN VÀ BẤT BIẾN TRONG PHƯƠNG<br /> PHÁP CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH .......... 7<br /> 4.1 BIẾN ......................................................................................................... 7<br /> 4.1.1 Khái niệm ......................................................................................... 7<br /> 4.1.2 Phương pháp tìm biến .................................................................... 7<br /> 4.2 BẤT BIẾN ................................................................................................. 8<br /> 4.2.1 Bất biến vòng lặp ............................................................................. 8<br /> <br /> ii<br /> <br /> 4.2.2 Một cách nhìn mang tính xây dựng ............................................. 10<br /> 4.2.3 Ví dụ cơ bản ................................................................................... 10<br /> 4.2.4 Phân loại bất biến: ........................................................................ 11<br /> 4.3.2 Tìm kiếm ........................................................................................ 13<br /> 4.3.3 Sắp xếp ........................................................................................... 13<br /> 4.4 ỨNG DỤNG KINH NGHIỆM TÌM BIẾN, BẤT BIẾN TRONG MỘT SỐ BÀI<br /> TẬP. .............................................................................................................. 13<br /> CHƯƠNG 5. KẾT LUẬN ............................................................................... 21<br /> 5.1 KẾT LUẬN .............................................................................................. 21<br /> 5.2 HẠN CHẾ VÀ KIẾN NGHỊ........................................................................ 22<br /> TÀI LIỆU THAM KHẢO ............................................................................... 23<br /> <br /> DANH MỤC CÁC HÌNH VẼ<br /> Hình 4. 1 . Các vòng lặp như là một sự tính toán bằng cắp xấp xỉ ................. 10<br /> Hình 4. 2. Ước số chung lớn nhất của hai số nguyên dương a và b ................ 11<br /> Hình 4. 3. Số lớn nhất với vòng lặp một biến .................................................. 13<br /> Hình 4. 5. Tìm kiếm trong một mảng chưa được sắp xếp. Error! Bookmark not<br /> defined.<br /> <br /> iii<br /> <br /> iv<br /> <br /> CHƯƠNG 1. MỞ ĐẦU<br /> Lý do chọn đề tài<br /> Trong suốt quá trình bản thân tôi được học tập, nghiên cứu tại trường<br /> Đại học Công nghệ, Đại học Quốc Gia Hà Nội đã được tiếp xúc với nhiều kiến<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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<br /> 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ả<br /> 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ã.<br /> 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<br /> chất rất quan trọng đó là tính đúng đắn.<br /> Việc chứng mình một chương trình là đúng đắn có nhiều phương pháp,<br /> trong phần nghiên cứu của luận văn, tôi chọn nghiên cứu Hoare logic (logic<br /> Hoare). Logic Hoare được Hoare xuất bản trong một bài báo năm 1969. Nó thực<br /> 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<br /> dụng logic Hoare để kiểm tra tính đúng của chương trình vẫn đang được tiến<br /> 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<br /> minh tính đúng logic Hoare đã gợi mở cho tôi một hướng nghiên cứu. Trong đó,<br /> 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<br /> 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<br /> 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<br /> 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ó.<br /> Mục đích nghiên cứu<br /> Đối tượng và phạm vi nghiên cứu<br /> Kết cấu của luận văn<br /> Gồm có 5 chương:<br /> Chương 1. Mở đầu. Giới thiệu lý do chọn đề tài, mục đích nghiên cứu,<br /> đối tượng và phạm vi nghiên cứu, kết cấu của luận văn.<br /> <br /> 1<br /> <br />