Luận văn được tiến hành và đã đạt được một số kết quả như sau: Tìm hiểu về bài toán chứng minh tính đúng đắn của chu trình bằng phương pháp logic Hoare; nghiên cứu các kỹ thuật tìm biến và bất biến cho việc sử dụng logic Hoare để chứng minh tính đúng đắn của chu trình; ứng dụng các kỹ thuật vào việc tìm kiếm biến và bất biến trong một hệ thống các bài toán cơ bả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 Ngành: Công nghệ Thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 TÓM TẮT 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 i MỤC LỤC MỤC LỤC II DANH MỤC CÁC HÌNH VẼ . III CHƯƠNG 1. MỞ ĐẦU . 1 LÝ DO CHỌN ĐỀ TÀI 1 MỤC ĐÍCH NGHIÊN CỨU . 1 ĐỐI TƯỢNG VÀ PHẠM VI NGHIÊN CỨU . 1 KẾT CẤU CỦA LUẬN VĂN 1 CHƯƠNG 2. TỔNG QUAN VỀ LOGIC HOARE . 2 . LOGIC VỊ TỪ . 2 . NHỮNG HIỂU BIẾT VỀ LOGIC HOARE . 2 Lịch sử của logic Hoare: . 2 . Nội dung của logic Hoare 2 . Các tiên đề của logic Hoare: 2 CHƯƠNG 3. CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH BẰNG LOGIC HOARE 4 PHƯƠNG PHÁP CHỨNG MINH 4 CÁC VÍ DỤ CHỨNG MINH .
