Xem trước tài liệu

Đang tải tài liệu...

Thông tin chi tiết tài liệu

Định dạng: PDF
Số trang: 66 trang
Dung lượng: Đang cập nhật

Giới thiệu nội dung

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

Tác giả:

Nguyễn Minh Hải

Lĩnh vực:

Luận văn Thạc sĩ Công nghệ Thông tin, Chuyên ngành: Kỹ thuật phần mềm

Nội dung tài liệu:

Luận văn này tập trung vào việc phát triển các kỹ thuật để tìm bất biến (invariants) và biến (variants) nhằm ứng dụng logic Hoare để chứng minh tính đúng đắn của các lệnh chu trình. Tài liệu đi sâu vào việc phân tích bản chất của vòng lặp thông qua bất biến vòng lặp, cung cấp lý thuyết và bài toán áp dụng trên các thuật toán cơ bản. Mục đích chính là cung cấp kiến thức và phương pháp để kiểm tra tính đúng đắn của chương trình, đặc biệt là các lệnh chu trình.

Mục lục chi tiết:

1. Mở đầu
2. Tổng quan về Logic Hoare
3. Chứng minh tính đúng đắn của lệnh chu trình bằng Logic Hoare
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
5. Kết luận