Khóa luậ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

hĩa ở trong 2.4.2. 
 - 59 - 
 CHƯƠNG 6. TÍNH ĐÚNG ĐẮN 
Một chương trình được cho cùng với chú thích của nó, hệ chứng minh quy định một số 
kiểm chứng các điều kiện đối với các kiểu khác nhau của các khẳng định và các cấu 
trúc chương trình. Tính đúng đắn của hệ chứng minh có nghĩa là đối với một phác thảo 
chứng minh thỏa mãn kiểm chứng các điều kiện, tất cả các cấu hình có thể đạt được 
trong các ngữ nghĩa của toán tử thỏa mãn các khẳng định được cho. 
Để thuận tiện, ta giới thiệu các chú thích sau: Một chương trình được cho prog, 
ta viết prog hoặc  cho chú thích của nó, và viết |prog , nếu prog thỏa mãn tất cả 
các yêu cầu được phát biểu trong các khẳng định, và '|' prog , nếu prog’ với chú 
thích ' thỏa mãn kiểm chứng các điều kiện của hệ chứng minh: 
Định nghĩa 6.0.1. Một chương trình được cho prog với chú thích  , thì |prog khi 
và chỉ khi với tất cả các cấu hình có thể đạt được ,T của prog, với tất cả 
  Tstm ,,  , và với tất cả các môi trường logic  chỉ tham chiếu tới các giá trị đang 
tồn tại trong  : 
1.    stmpreL|,,  , và 
2. GIG|, . 
Hơn nữa, với tất cả các lớp c, các đối tượng   cVal , và các trạng thái cục bộ 
' : 
3.   cL I|',,  . 
Đối với các phác thảo chứng minh, ta viết '|' prog khi và chỉ khi prog’ với chú 
thích ' thỏa mãn kiểm chứng các điều kiện của hệ chứng minh. 
6.1. Tính đúng đắn 
Tính đúng đắn có nghĩa là tất cả các cấu hình có thể đạt được thỏa mãn các khẳng định 
của chúng đối với một chương trình được chú thích – được kiểm chứng bằng sử dụng 
chứng minh các điều kiện. Tính đúng đắn của một phương thức được chứng minh 
bằng một quy nạp đơn giản trong số của các bước tính toán. 
 - 60 - 
Trước khi bắt tay vào trình bày tính đúng đắn và chứng minh của nó, ta cần hiểu 
rõ mối quan hệ giữa chương trình gốc và phác thảo chứng minh, có nghĩa là, chương 
trình gốc được mở rộng bằng các biến phụ trợ, và được bao bọc với các khẳng định. 
Để tạo sự rõ ràng trong mối quan hệ giữa chương trình gốc và phác thảo chứng 
minh, ta định nghĩa một toán tử chiếu prog , xóa tất cả các phần thêm vào của sự 
biến đổi. Cho prog’ là một phác thảo chứng minh với prog, và ',' T là một cấu hình 
toàn cục của prog’. Thì prog' được định nghĩa bởi bỏ đi tất cả các biến thể hiện 
phụ trợ từ các miền trạng thái thể hiện. Với tập các cấu hình luồng, progT ' được cho 
bởi hạn chế các miền của các trạng thái cục bộ để không có các biến phụ trợ và bỏ đi 
tất cả các bổ sung. Thêm vào đó, với các cấu hình cục bộ   ',, ! Tstmreturn retgetlock  , 
nếu luồng đang thi hành ở trong tập đợi, nghĩa là, nếu      waitnthread  ',  với 
một số n nào đó, thì lệnh getlockreturn được thay thế bằng getlockreturnsignal;? . Hơn nữa, 
với các cấu hình cục bộ   '';,, ! Tstmreturnstm ret  với stm một phép gán phụ 
trợ trong phương thức notify hoặc trong phương thức notifyAll, phép gán phụ trợ stm 
được thay thế theo thứ tự bằng !signal và !signal_all. Bổ đề sau biểu thị rằng nếu sự 
biến đổi không thay đổi hành vi của các chương trình: 
Bổ đề 6.1.1. Cho prog’ là một phác thảo chứng minh với một chương trình prog. Thì 
,T là một cấu hình có thể đạt được của prog khi và chỉ khi tồn tại một cấu hình có 
thể đạt được ',' T của prog’ với  ,',' TprogprogT  . 
Bổ đề 6.1.2. (Định danh) Cho ,T là một cấu hình có thể đạt được của một phác 
thảo chứng minh. Thì: 
1. với tất cả các ngăn xếp  và ' trong T và với tất cả các cấu hình cục bộ 
   stm,, và   '',','  stm ta có    threadthread '  khi và chỉ khi '  , và 
2. với mỗi ngăn xếp    nnn stmstm ,,...,, 000  trong T và các chỉ số nji  ,0 , 
(a)   0 threadi ; 
(b) i < j và ji   kéo theo       counterconfconf iji   , 
(c) 0 < j kéo theo       threadconfcaller jjjj 111 ,,   , và 
(d)     threadcallerproj 00 3,   , 
 - 61 - 
trong đó  ivproj , là thành phần thứ i của bộ v. 
Bổ đề sau phát biểu rằng luồng sở hữu khóa, và các tập đợi và tập được thông 
báo của các ngữ nghĩa được trình bày bởi các biến lock, wait, và notified. Hơn nữa, bổ 
đề đảm bảo rằng tính phân đoạn của các dãy được lưu trữ trong các biến wait và 
notified; nếu thứ tự của các phần tử không quan trọng, ta sử dụng tập ký hiệu cho các 
giá trị của chúng. 
Bổ đề 6.1.3. (Lock, Wait, Notify) Cho ,T là một cấu hình có thể đạt được của một 
phác thảo chứng minh với chương trình gốc prog,   Val là một định danh đối 
tượng, và cho   Tstm  ',, 000   . Hơn nữa cho n là số của các thi hành phương 
được đồng bộ của  trong  , nghĩa là, n =   |.|,,| synchrstmstm   . Thì: 
1. (a)  ,progTowns  khi và chỉ khi    freelock  
(b)   ,progowns  khi và chỉ khi     nlock ,0  
2. (a)   ,progTwait  khi và chỉ khi     waitn  ,0 
(b)   ,progTnotified  khi và chỉ khi     notifiedn  ,0 
(c)     1,iwaitproj  =     1,jwaitproj  kéo theo i = j 
(d)     1,inotifiedproj  =     1,jnoitifiedproj  kéo theo i = j 
(e) nếu     waitm  ,0 hoặc     notifiedm  ,0 thì m = n 
(f)      notifiedwait    
trong đó  is là thành phần thứ i của dãy s. 
Cuối cùng, biến thể hiện phụ trợ started của một đối tượng lưu trữ nếu luồng của 
đối tượng đã được khởi động hoặc không: 
Bổ đề 6.1.4. (Started) Đối với tất cả các cấu hình có thể đạt được ,T của một phác 
thảo chứng minh cho một chương trình prog, và tất cả các đối tượng   Val , ta có 
 ,progTstarted  khi và chỉ khi   started . 
Cho prog là một chương trình với chú thích  , và prog’ một phác thảo chứng 
minh tương ứng với chú thích ' . Cho GI’ là bất biến toàn cục của ' , 'cI biểu thị các 
 - 62 - 
bất biến lớp của nó, và với một khẳng định p của  cho p’ biểu thị khẳng định của ' 
được kết hợp với cùng điểm điều khiển. Ta viết '|  khi và chỉ khi GIGIG  '| , 
ccL II  '| đối với tất cả các lớp c, và '| ppL  , đối với tất cả các khẳng định p của 
 được kết hợp với các điểm điều khiển nào đó. Để cho các biến phụ trợ ngữ nghĩa, 
các kéo theo ở trên được ước lượng trong ngữ cảnh của các trạng thái của chương trình 
được bổ sung. Định lý sau phát biểu tính đúng đắn của phương pháp chứng minh. 
Định lý 6.1.5. (Tính đúng đắn) Cho prog’ là một phác thảo chứng minh với chú thích 
'prog . 
Nếu '|' progprog  thì '|' progprog  
Chứng minh tính đúng đắn bao gồm một chứng minh quy nạp trong chiều dài của 
tính toán, đồng thời trong tất cả ba phần từ định nghĩa 6.0.1. Đối với bước quy nạp, ta 
giả thiết rằng kiểm chứng các điều kiện được thỏa mãn và giả thiết một cấu hình có thể 
đạt được thỏa mãn chú thích. Ta tạo trường hợp khác biệt trong cú pháp của bước tính 
toán kế tiếp: 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ỏ bằng sử dụng 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ỏ với sự giúp đỡ của của 
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. 
Định lý 6.1.5 được đưa ra đối với tính có thể đạt được của các chương trình được 
bổ sung. Với sự giúp đỡ của bổ đề 6.1.1, ta có ngay lập tức : 
Hệ quả 6.1.6. Nếu '|' progprog  và progprog   '| , thì progprog | . 
 - 63 - 
KẾT LUẬN 
Với sự phát triển không ngừng của nhu cầu tính toán, xử lý số liệu, khai phá 
thông tin thì lập trình đa luồng ngày càng quan trọng và là một phần không thể thiếu 
trong các hệ thống tính toán, cũng như trong các hệ thống ứng dụng. Sự quan trọng và 
cần thiết của việc kiểm chứng tính đúng của chương trình luôn được quan tâm đúng 
mức do vai trò to lớn của nó. Kiểm chứng tính đúng đắn của chương trình Java đa 
luồng không chỉ mang ý nghĩa về mặt lý thuyết của kiểm chứng mà nó thực sự có vai 
trò không thể thiếu trong thực tế, qua đó giúp ta tránh được những sai lầm, thiếu sót dù 
là rất nhỏ nhưng có thể dẫn tới những hậu quả thật khó lường. Trong các hệ thống đòi 
hỏi tính an toàn cao như các hệ thời gian thực, các hệ mô phỏng, hoặc các hệ thống 
giám sát vệ tinh, máy bay thì kiểm chứng tính đúng đắn của các chương trình mang 
một ý nghĩa vô cùng to lớn. Nó cho phép xác định được tính đúng đắn của chương 
trình từ các giả thiết và các khẳng định ban đầu mà không cần phải chứng thực điều đó 
khi chạy chương trình, mà nếu trong thực tế chương trình chạy sai gây ra hậu quả vô 
cùng nghiêm trọng. 
Phương pháp kiểm chứng trên còn được sử dụng để chứng minh tính không có 
deadlock của một chương trình Java. Phác thảo chứng minh của chương trình nếu thỏa 
mãn các điều kiện của chứng minh tính không có deadlock thì chương trình sẽ không 
có deadlock. 
Để có thể kiểm chứng tính đúng đắn của một chương trình Java đa luồng, ta có 
thể sử dụng phương pháp đã trình bày ở trên. Nó là cơ sở, tiền đề để xây dựng các 
công cụ hỗ trợ việc kiểm chứng tự động. Do thời gian thực hiện đề tài có hạn và phạm 
vi rộng lớn của đề tài, khóa luận chưa đề cập hết được các phương pháp cũng như kỹ 
thuật hiện đại kiểm chứng tính đúng đắn của chương trình, cũng như các công cụ hỗ 
trợ kiểm chứng hiện nay. 
 - 64 - 
TÀI LIỆU THAM KHẢO 
[1] Erika Abraham - An Assertional Proof System for Multitheaded Java – 
Theory and Tool Support 
WEBSITE: 
[2]  
[3]