- 1 -
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
- 2 -
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.
- 3 -
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 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 -
MỞ ĐẦU
Yêu cầu của người dùng đối với một phần mềm ngày nay là không những nó phải có
giao diện đẹp, tốc độ xử lý dữ liệu nhanh, tốc độ phản ứng của chương trình với người
dùng cũng là một yêu cầu không thể bỏ qua. Một chương trình yêu cầu vừa có giao
diện đẹp, vừa xử lý nhanh chạy trên một máy cấu hình bình thường thì cần có một cơ
chế để quản lý cấp phát tài nguyên của máy một cách phù hợp. Và cơ chế quản lý đa
luồng chính là một giải pháp cho các yêu cầu trên. Ngôn ngữ lập trình Java là một
ngôn ngữ lập trình bậc cao hỗ trợ rất mạnh cho lập trình đa luồng, được sử dụng nhiều
trong các hệ thống lớn cũng như trong các phần mềm có quy mô vừa và nhỏ.
Trong các hệ thống lớn, chỉ một lỗi rất nhỏ cũng có thể dẫn tới những kết quả tai
hại, hoặc thậm chí là phá hủy hệ thống. Do đó ta thấy được tính quan trọng đối với
việc kiểm chứng tính đúng đắn của một chương trình. Việc kiểm chứng tính đúng đắn
của một chương trình Java đa luồng là không thể thiếu được trong việc phát triển hệ
thống. Ta cần có một phương pháp kiểm chứng tính đúng đắn của một chương trình
Java đa luồng. Đó chính là phương pháp thông qua sử dụng logic Hoare.
Logic Hoare là một hệ thống hình thức được phát triển bởi các nhà khoa học máy
tính Anh C.A.R.Hoare, và về sau được cải tiến bởi Hoare và các nhà nghiên cứu khác.
Mục đích của hệ thống này là cung cấp một tập các quy tắc logic để lý luận về tính
đúng đắn của các chương trình máy tính với tính chính xác của các logic toán học.
Logic Hoare là cơ sở để định nghĩa tính đúng đắn của hệ thống.
Trong khóa luận tốt nghiệp này em sẽ trình bày về 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.
Khóa luận sẽ có sáu chương với nội dung chính như sau:
Chương 1: Logic Hoare
Chương 2: Ngôn ngữ tuần tự
- 5 -
Chương 3: Ngôn ngữ tương tranh
Chương 4: Bộ điều phối lặp lại
Chương 5: Phép toán trước yếu nhất
Chương 6: Tính đúng đắn
Tuy nhiên do còn nhiều hạn chế về thời gian cũng như kiến thức của bản thân,
khóa luận này không thể tránh khỏi những thiếu sót. Em rất mong nhận được sự quan
tâm góp ý của các thầy, cô giáo cũng như các anh, chị và các bạn, những người quan
tâm đến vấn đề này.
Em xin chân thành cảm ơn thầy giáo, tiến sỹ Đặng Văn Hưng, người đã hướng
dẫn trực tiếp, động viên và giúp đỡ em rất nhiều để hoàn thành khóa luận này.
Cuối cùng, em xin bày tỏ lòng biết ơn sâu sắc tới gia đình, bạn bè, các thầy cô
giáo, những người đã quan tâm, giúp đỡ em rất nhiều trong suốt những năm ngồi trên
ghế nhà trường.
Hà Nội, tháng 5 năm 2009
Sinh viên
LÊ VĂN VIỄN