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<br /> (INVARIANTS) VÀ BIẾN (VARIANTS) CHO VIỆC<br /> SỬ DỤNG HOARE LOGIC ĐỂ CHỨNG MINH TÍNH<br /> ĐÚNG ĐẮN CỦA CHU TRÌNH<br /> <br /> LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN<br /> <br /> Hà Nội – 2016<br /> <br /> ĐẠ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<br /> (INVARIANTS) VÀ BIẾN (VARIANTS) CHO VIỆC<br /> SỬ DỤNG HOARE LOGIC ĐỂ CHỨNG MINH TÍNH<br /> ĐÚ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 /> <br /> LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN<br /> NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. ĐẶNG VĂN HƯNG<br /> <br /> Hà Nội - 2016<br /> 1<br /> <br /> 2<br /> <br /> LỜI CẢM ƠN<br /> Trước tiên, tôi xin chân thành cảm ơn TS. Đặng Văn Hưng, người thầy đã<br /> 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<br /> thành luận văn tốt nghiệp.<br /> 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<br /> 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,<br /> 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<br /> tập và nghiên cứu tại Trường.<br /> 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à<br /> đà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<br /> trình độ chuyên môn.<br /> 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<br /> K21 Công nghệ phần mềm đã thường xuyên quan tâm, giúp đỡ, chia sẻ kinh<br /> nghiệm, tài liệu hữu ích trong suốt quá trình học tập.<br /> 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ả<br /> mọi người.<br /> <br /> Hà Nội, tháng 11 năm 2016<br /> Tác giả luận văn<br /> <br /> Nguyễn Minh Hải<br /> <br /> 1<br /> <br /> LỜI CAM ĐOAN<br /> 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)<br /> và biến (variants) cho việc sử dụng Hoare Logic để chứng minh tính đúng đắn của<br /> 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,<br /> 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<br /> 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<br /> đề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<br /> từ bất kì một nguồn tài liệu nào khác.<br /> Nếu có gì sai sót, tôi xin chịu mọi trách nhiệm.<br /> <br /> Hà Nội, tháng 11 năm 2016<br /> Tác giả luận văn<br /> <br /> Nguyễn Minh Hải<br /> <br /> 2<br /> <br />