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

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.
Nội dung trích xuất từ tài liệu:
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ỘITRƯỜNG ĐẠI HỌC CÔNG NGHỆNGUYỄN MINH HẢIPHÁT TRIỂN CÁC KỸ THUẬT TÌM BẤT BIẾN(INVARIANTS) VÀ BIẾN (VARIANTS) CHO VIỆCSỬ DỤNG HOARE LOGIC ĐỂ CHỨNG MINH TÍNHĐÚNG ĐẮN CỦA CHU TRÌNHLUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TINHà Nội – 2016ĐẠI HỌC QUỐC GIA HÀ NỘITRƯỜNG ĐẠI HỌC CÔNG NGHỆNGUYỄN MINH HẢIPHÁT TRIỂN CÁC KỸ THUẬT TÌM BẤT BIẾN(INVARIANTS) VÀ BIẾN (VARIANTS) CHO VIỆCSỬ DỤNG HOARE LOGIC ĐỂ CHỨNG MINH TÍNHĐÚNG ĐẮN CỦA CHU TRÌNHNgành: Công nghệ Thông tinChuyên ngành: Kỹ thuật phần mềmMã số: 60480103LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TINNGƯỜI HƯỚNG DẪN KHOA HỌC: TS. ĐẶNG VĂN HƯNGHà Nội - 201612LỜI CẢM ƠNTrướ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ànthà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ôngtin, 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ọctậ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 caotrì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ớpK21 Công nghệ phần mềm đã thường xuyên quan tâm, giúp đỡ, chia sẻ kinhnghiệ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 2016Tác giả luận vănNguyễn Minh Hải1LỜI CAM ĐOANTô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ủachu 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àytrong 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ảntừ 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 2016Tác giả luận vănNguyễn Minh Hải2