Đang chuẩn bị nút TẢI XUỐNG, xin hãy chờ
Tải xuống
Có rất nhiều phương pháp để kiểm chứng tính đúng đắn của một chương trình Java đa luồng. Một trong các phương pháp đó là sử dụng logic Hoare. Kiểm chứng tính đúng đắn của một chương trình Java đa luồng sử dụng logic Hoare yêu cầu ta cần phải chứng minh một chương trình được bổ sung và chú thích dưới sự thi hành của các lệnh phải thỏa mãn: Nếu bước tính toán thi hành một phép gán, thì ta sử dụng các điều kiện tính đúng đắn cục bộ để chứng minh tính quy nạp của sự. | TRƯỜNG KHOA. . . Báo cáo tôt nghiệp Đê tài 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 Hoare - 1 - TÓM TẮT KHÓA LUẬN Có rất nhiều phương pháp để kiểm chứng tính đúng đắn của một chương trình Java đa luồng. Một trong các phương pháp đó là sử dụng logic Hoare. Kiểm chứng tính đúng đắn của một chương trình Java đa luồng sử dụng logic Hoare yêu cầu ta cần phải chứng minh một chương trình được bổ sung và chú thích dưới sự thi hành của các lệnh phải thỏa mãn Nếu bước tính toán thi hành một phép gán thì ta sử dụng các điều kiện tính đúng đắn cục bộ để chứng minh tính quy nạp của sự thi hành các thuộc tính của cấu hình cục bộ và kiểm tra tính không có can thiệp đối với tất cả các cấu hình cục bộ khác và các bất biến lớp khác. Đối với giao tiếp tính bất biến đối với thi hành các đối tác và bất biến toàn cục được chứng tỏ thông qua kiểm tra sự hợp tác đối với giao tiếp. Giao tiếp với chính nó không ảnh hưởng trạng thái toàn cục tính bất biến của các thuộc tính còn lại dưới các quan sát tương ứng được chứng tỏ thông qua kiểm tra tính không có can thiệp. Cuối cùng đối với tạo đối tượng tính bất biến đối với bất biến toàn cục tạo cấu hình cục bộ bất biến lớp của đối tượng được tạo được đảm bảo các điều kiện của kiểm tra hợp tác đối với tạo đối tượng tất cả các thuộc tính khác được chứng tỏ là bất biến thông qua sử dụng kiểm tra tính không có can thiệp. - 2 - MỤC LỤC 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 .
