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 Hoare

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ự...
Nội dung trích xuất từ tài liệu:
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 Hoare 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ẬNCó 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 đaluồ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ảichứ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ệnhphả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ệntí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ủacấ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 đốitá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ácthuộ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ínhkhô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ếntoà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 đượcchứ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ỤCTÓ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... ...