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

- 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

- 6 -

CHƯƠNG 1. LOGIC HOARE

1.1. Logic vị từ

Định nghĩa: Vị từ là một hàm nhận một giá trị Bool.

Một vị từ thực sự là một giá trị logic được biểu hiện bằng tham số. Nó có thể đúng với

một số đối số, và sai với một số đối số khác. Chẳng hạn x > 0 là một vị từ với một đối

số, ta có thể đặt tên nó là gt0(x). Do vậy mà gt0(5) là đúng và gt0(0) là sai.

Định nghĩa: Các thành phần của logic vị từ wffs gồm có các thành phần sau:

• Các định danh biến – một tập (thường là vô hạn) của các tên biến, thường

là , , ,..., , , ,... 1 2 1 2

x x x y y y

• Các định danh hằng – một tập (hữu hạn, vô hạn, hoặc rỗng) của các tên hằng,

thường là , , ,..., , , ... 1 2 1 2

a a a b b b

• Các định danh vị từ – một tập (không rỗng) của các tên vị từ, thường

là , , , ..., , , ... p p1 p 2 q q1 q2

• Các định danh hàm – một tập các tên hàm, thường

là , , , ..., , , , ... 1 2 g g1 g 2

f f f

Mỗi định danh hàm và định vị từ có một số cố định của các đối số mà nó chấp nhận là

arity.

Định nghĩa: Các toán hạng của logic vị từ được định nghĩa một cách đệ quy như sau:

(i) các tên biến và các tên hằng là toán hạng, và

(ii) nếu k

t ,...,t

1

là các toán hạng và f là một tên hàm có số các đối số cố định là k,

thì   k

f t ,t ,...,t

1 2

là một toán hạng