Luận Văn Phương pháp kiểm chứng tính đúng đắn của một chương trình Java đa luồng thông qua sử dụng logic Hoar

TÓM TẮT KHÓA LUẬN - 1 -
MỞ ĐẦU - 4 -
CHƯƠNG 1. LOGIC HOARE - 6 -
1.1. Logic vị từ - 6 -
1.2. Các tiên đề của Logic Hoare .- 9 -
1.2.1. Các công thức đúng cú pháp cho chứng minh chương trình - 9 -
1.2.2. Tiên đề của phép gán - 10 -
1.2.3. Các quy tắc bổ sung - 10 -
CHƯƠNG 2. NGÔN NGỮ TUẦN TỰ - 12 -
2.1. Cú pháp .- 13 -
2.2. Ngữ nghĩa - 16 -
2.2.1. Trạng thái và các cấu hình .- 16 -
2.2.2. Các ngữ nghĩa toán tử - 18 -
2.3. Ngôn ngữ khẳng định - 20 -
2.3.1. Cú pháp - 20 -
2.3.2. Ngữ nghĩa - 21 -
2.4. Hệ chứng minh - 25 -
2.4.1. Phác thảo chứng minh - 26 -
2.4.2. Kiểm chứng các điều kiện - 31 -
CHƯƠNG 3. NGÔN NGỮ TƯƠNG TRANH Error! Bookmark not defined.
3.1. Cú pháp .- 42 -
3.2. Ngữ nghĩa - 42 -
3.3. Hệ chứng minh - 43 -
3.3.1. Phác thảo chứng minh - 43 -
3.3.2. Kiểm chứng các điều kiện - 43 -
CHƯƠNG 4. BỘ ĐIỀU PHỐI LẶP LẠI . Error! Bookmark not defined.
4.1. Cú pháp .- 47 -
4.2. Ngữ nghĩa - 47 -
4.3. Hệ chứng minh .- 48-
4.3.1. Phác thảo chứng minh - 49 -
4.3.2. Kiểm chứng các điều kiện - 51 -
CHƯƠNG 5. PHÉP TOÁN ĐIỀU KIỆN TRƯỚC YẾU NHẤT - 53 -
5.1. Các phép toán thay thế - 54 -
5.2. Kiểm chứng các điều kiện .- 54-
CHƯƠNG 6. TÍNH ĐÚNG ĐẮN . Error! Bookmark not defined.
6.1. Tính đúng đắn .- 59 -
KẾT LUẬN - 62-
TÀI LIỆU THAM KHẢO - 63-
- 4 -