Luận Văn 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 Hoare

MỤC LỤC
TÓM TẮT KHÓA LUẬN -1
-MỞ ĐẦU -4 -
CHƯƠNG 1. LOGICHOARE -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 .
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 .
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 .
6.1. Tính đúng đắn . -59 -
KẾT LUẬN -62-
TÀI LIỆU THAM KHẢO - 63-