Nội dung luận án gồm có 5 chương: Chương 1/ 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 3/ Chứng minh tính đúng đắn của lệnh chu trình bằng logic Hoare, 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/ 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. | ĐẠ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 Hà Nội - 2016 1 2 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 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à
