Tóm tắt Luận văn Phát triển các kỹ thuật tìm bất biến (Invariants) và biến (Variants) cho việc sử dụng Hoare logic để chứng minh tính đúng đắn của chu trình

i ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN MINH HẢI PHÁT TRIỂN CÁC KỸ THUẬT TÌM BẤT BIẾN (INVARIANTS) VÀ BIẾN (VARIANTS) CHO VIỆC SỬ DỤNG HOARE LOGIC ĐỂ CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA CHU TRÌNH Ngành: Công nghệ Thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 TÓM TẮT LUẬN VĂN THẠC SĨ CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: TS. ĐẶNG VĂN HƯNG Hà Nội - 2016 ii MỤC LỤC MỤC LỤC ........................................................................................................ II DANH MỤC CÁC HÌNH VẼ ......................................................................... III CHƯƠNG 1. MỞ ĐẦU ..................................................................................... 1 LÝ DO CHỌN ĐỀ TÀI ...................................................................................... 1 MỤC ĐÍCH NGHIÊN CỨU ............................................................................... 1 ĐỐI TƯỢNG VÀ PHẠM VI NGHIÊN CỨU ......................................................... 1 KẾT CẤU CỦA LUẬN VĂN .............................................................................. 1 CHƯƠNG 2. TỔNG QUAN VỀ LOGIC HOARE ........................................... 2 2.1. LOGIC VỊ TỪ ........................................................................................... 2 2.2. NHỮNG HIỂU BIẾT VỀ LOGIC HOARE ................................................... 2 2.2.1 Lịch sử của logic Hoare: ................................................................. 2 2.2.2. Nội dung của logic Hoare .............................................................. 2 2.2.3. Các tiên đề của logic Hoare: .......................................................... 2 CHƯƠNG 3. CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH BẰNG LOGIC HOARE .................................................................................... 4 3.1 PHƯƠNG PHÁP CHỨNG MINH .................................................................. 4 3.2 CÁC VÍ DỤ CHỨNG MINH :....................................................................... 5 3.2.1 Bài 1 .................................................................................................. 5 3.2.2 Bài 2 .................................................................................................. 6 CHƯƠNG 4. NGHIÊN CỨU VỀ BIẾN VÀ BẤT BIẾN TRONG PHƯƠNG PHÁP CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH .......... 7 4.1 BIẾN ......................................................................................................... 7 4.1.1 Khái niệm ......................................................................................... 7 4.1.2 Phương pháp tìm biến .................................................................... 7 4.2 BẤT BIẾN ................................................................................................. 8 4.2.1 Bất biến vòng lặp ............................................................................. 8 iii 4.2.2 Một cách nhìn mang tính xây dựng ............................................. 10 4.2.3 Ví dụ cơ bản ................................................................................... 10 4.2.4 Phân loại bất biến: ........................................................................ 11 4.3.2 Tìm kiếm ........................................................................................ 13 4.3.3 Sắp xếp ........................................................................................... 13 4.4 ỨNG DỤNG KINH NGHIỆM TÌM BIẾN, BẤT BIẾN TRONG MỘT SỐ BÀI TẬP. .............................................................................................................. 13 CHƯƠNG 5. KẾT LUẬN ............................................................................... 21 5.1 KẾT LUẬN .............................................................................................. 21 5.2 HẠN CHẾ VÀ KIẾN NGHỊ ........................................................................ 22 TÀI LIỆU THAM KHẢO ............................................................................... 23 DANH MỤC CÁC HÌNH VẼ Hình 4. 1 . Các vòng lặp như là một sự tính toán bằng cắp xấp xỉ ................. 10 Hình 4. 2. Ước số chung lớn nhất của hai số nguyên dương a và b ................ 11 Hình 4. 3. Số lớn nhất với vòng lặp một biến .................................................. 13 Hình 4. 5. Tìm kiếm trong một mảng chưa được sắp xếp. Error! Bookmark not defined. iv 1 CHƯƠNG 1. MỞ ĐẦU Lý do chọn đề tài Trong suốt quá trình bản thân tôi được học tập, nghiên cứu tại trường Đại học Công nghệ, Đại học Quốc Gia Hà Nội đã được tiếp xúc với nhiều kiến thức mới, quan trọng, được ứng dụng mạnh mẽ trong các lĩnh vực rộng lớn của CNTT. Là một giáo viên giảng dạy bộ môn tin học tại cấp THPT, tôi thường xuyên tiếp xúc và hướng dẫn học sinh những kiến thức cơ bản về ngôn ngữ lập trình trên cơ sở là ngôn ngữ Pascal. Do đó, tôi đặc biệt có hứng thú với bộ môn kiểm thử. Việc kiểm tra một chương trình xem nó có đúng, chạy tốt, phù hợp với yêu cầu của người lập trình hay không luôn là một vấn đề quan trọng, mang tính thời đại đối với mọi lập trình viên cũng như các nhà quản lý phần mềm. Cả dự án có thể bị ảnh hưởng nếu gặp những lỗi nghiêm trọng trong việc viết mã. Trong những tính chất đảm bảo chương trình phù hợp với yêu cầu, có một tính chất rất quan trọng đó là tính đúng đắn. Việc chứng mình một chương trình là đúng đắn có nhiều phương pháp, trong phần nghiên cứu của luận văn, tôi chọn nghiên cứu Hoare logic (logic Hoare). Logic Hoare được Hoare xuất bản trong một bài báo năm 1969. Nó thực sự đã được ra đời rất lâu, nhưng bản thân nó luôn mang tính thời đại vì việc áp dụng logic Hoare để kiểm tra tính đúng của chương trình vẫn đang được tiến hành thường xuyên trên phạm vi rộng lớn. Việc tìm hiểu về phương pháp chứng minh tính đúng logic Hoare đã gợi mở cho tôi một hướng nghiên cứu. Trong đó, tôi đi xâu vào việc phân tích về Biến (Variants) và Bất biến (Invariants), hai yếu tố quan trọng đầu tiên trong việc chứng minh tính đúng của lệnh chu trình. Bản chất của một vòng lặp luôn có sự ẩn chứa của một bất biến vòng lặp. Hay nói cách khác, bạn không thể hiểu được vòng lặp nếu chưa biết về bất biến của nó. Mục đích nghiên cứu Đối tượng và phạm vi nghiên cứu Kết cấu của luận văn Gồm có 5 chương: Chương 1. Mở đầu. Giới thiệu lý do chọn đề tài, mục đích nghiên cứu, đối tượng và phạm vi nghiên cứu, kết cấu của luận văn. 2 Chương 2. Tổng quan về logic Hoare. Chương này cung cấp những lý thuyết cơ bản về logic vị từ và logic Hoare. Chương 3. Chứng minh tính đúng đắn của lệnh chu trình bằng logic Hoare. Trong chương cung cấp những cách thức cơ bản để chứng minh tính đúng đắn. Bên cạnh đó, tôi thực hiện áp dụng thực tế các lý thuyết vào việc chứng minh trong một vài bài tập cơ bản. Chương 4. Nghiên cứu về biến và bất biến trong phương pháp chứng minh tính đúng đắn của lệnh chu trình. Ứng dụng vào tìm biến và bất biến trong một số thuật toán cơ bản. Chương 5. Kết luận. Chương tổng kết lại những vấn đề đạt được, chưa đạt được và những kiến nghị đề xuất của luận văn. CHƯƠNG 2. TỔNG QUAN VỀ LOGIC HOARE 2.1. Logic vị từ 2.2. Những hiểu biết về Logic Hoare 2.2.1 Lịch sử của logic Hoare: 2.2.2. Nội dung của logic Hoare Đặc điểm trung tâm của logic Hoare là bộ ba Hoare (Hoare Triples). Bộ ba này mô tả sự thực thi một đoạn mã có thể thay đổi trạng thái tính toán như thế nào. Một bộ ba hoare có dạng    P c Q . Trong đó P là điều kiện tiên quyết, Q là các hậu điều kiện, c là các lệnh chương trình. Ở đây P và Q là những công thức có dạng logic vị từ, chúng đưa ra những khảng định là đúng hoặc sai. Ý nghĩa của một bộ ba Hoare    P c Q có thể được giải thích như sau: Nếu tôi bắt đầu một trạng thái trong đó P đúng và thực hiện c thì c sẽ chấm dứt trong một trạng thái trong đó Q là đúng, chương trình cho kết quả đúng. Chú ý rằng trường hợp nếu c không dừng thì sẽ không có khái niệm Q, tức là Q có thể là bất cứ thứ gì. Như vậy, mọi người thường chọn Q là false để diễn tả rằng c không dừng. 2.2.3. Các tiên đề của logic Hoare: 3 Luật tiên đề rỗng  P skip  P với P là một công thức logic mệnh đề bất kỳ. Trong khi skip không làm gì, tôi thấy cái gì đúng sau khi nó thực hiện cũng như là cái đã đúng trước đó. Luật về phép gán Tôi giả thiết rằng x : E biểu thị một lệnh gán, trong đó x là một biến và E là một biểu thức thích hợp, P là một công thức logic vị từ. Khi đó, luật về phép gán được phát biểu như sau   /P x E x:=E  P Các quy tắc bổ trợ : Độ mạnh của các công thức đúng ngữ pháp: Nếu P và Q là hai công thức đúng ngữ pháp, mà 'P P thì khi đó tôi nói P là công thức mạnh hơn P’ và P’ thì yếu hơn P. Một điều kiện mạnh hơn là một điều kiện mà có ít các giá trị thỏa mãn nó hơn điều kiện kia. Độ mạnh của điều kiện trước:         ' ' ,P P' ' P c Q P c Q  c là một đoạn chương trình bất kỳ. Độ yếu của điều kiện sau:         ,Q ' ' P c Q Q P c Q  c là một đoạn chương trình bất kỳ. Luật ghép:           ; P S Q Q T R P S T R Luật điều kiện:            P B S Q P B T Q P if B then S else T Q   4 Luật While        w P B C P P hile B do C B P    Ở đây P là điều kiện bất biến của vòng lặp. Luật này chỉ chứng mình tính đúng đắn bộ phận của lệnh chu trình. Luật While dành cho tính đúng đắn toàn phần         0 w P B t N C P t N P t P hile B do C B P          Luật này dùng để chứng minh tính đúng đắn toàn phần của lệnh chu trình. Trong luật này, ngoài việc giữ các điều kiện của bất biến vòng lặp tôi còn phải chứng minh tính dừng bằng cách chứng minh giá trị của một số hạng (t) giảm dần sau mỗi lần lặp. t được gọi là biến, chú ý rằng t phải thuộc tập chắc chắn, để cho mỗi lần lặp có thể giảm đi một giá trị hữu hạn nào đó. CHƯƠNG 3. CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH BẰNG LOGIC HOARE 3.1 Phương pháp chứng minh Để xác minh tính chính xác một phần của các vòng lặp có dạng hình thức while b do c, tôi cần một bất biến I sao cho các điều kiện sau đây được thỏa mãn:  P I : Các bất biến bước đầu là đúng.     I b c I : Mỗi lần thực hiện vòng lặp luôn bảo tồn bất biến, tức là sau mỗi lần thực hiện thân vòng lặp thể hiện bất biến luôn được giữ nguyên.   I b Q  : Các bất biến và điều kiện thoát vòng lặp bao hàm hậu điều kiện. Tôi có thể xác minh đầy đủ tính đúng đắn của vòng lặp bằng cách đưa ra một biến chức năng có giá trị nguyên t, đáp ứng các điều kiện sau đây: 5  0I b t   : Nếu tôi đi vào thân vòng lặp (nghĩa là điều kiện lặp b được đánh giá đúng) và bất biến được bảo tồn, sau đó t phải được khảng định đúng. Tôi thấy 0t  nghĩa là biến chức năng có giá trị dương, điều đó cần được đảm bảo để có thể bắt đầu thân vòng lăp.     I b t N c t N    : Giá trị của biến chức năng sẽ giảm sau mỗi lần thực hiện thân vòng lặp (ở đây N là một hằng số). Công việc chứng minh tính đúng đắn đầy đủ của lệnh chu trình dựng trên những luận cứ của Hoare được thực hiện như sau: 0P I b t       I b t N c I t N      I b Q     P b do c Qwhile 3.2 Các ví dụ chứng minh : Trên thực tế, với hàng tỉ bài toán khác nhau, có những đặc điểm vô tận trong việc dùng vòng lặp có dạng thức while b do c để thể hiện. Để rèn luyện và làm rõ cách thức chứng minh tính đúng đắn dựa trên lý thuyết của Hoare, tôi sẽ lần lượt làm một vài ví dụ. Trong phần này, tôi sẽ thực hiện hai bài tập sau đây: 3.2.1 Bài 1 Tính tổng từ 1..n  1 0i s   while i n do ( : ; : 1)s s i i i    1 n j s j         Giải: tôi chọn được bất biến vòng lặp sẽ là 1 1 1 1 i j I i n s j         . tôi chọn được một biến chức năng là : 1t n i   . 6 Nhiệm vụ là lần lượt chứng minh các điều kiện sau đây là đúng để đảm bảo tính đúng đắn của lệnh chu trình trong bài tập nêu ra  1 0i s I    1 0I i n n i       1I i n n i N      : ; : 1s s i i i     1I n i N      1 n j I i n s j      Từ những lý luận kể trên, tôi có thể khảng định những bộ ba Hoare là đúng. Điều đó đồng nghĩa với việc tôi đã hoàn thành việc chứng minh tính đúng 3.2.2 Bài 2 Tính mr n  : 1; : 0r i  while i m do  r : r*n;i : i 1;    mr n Giải: Bất biến vòng lặp đầy đủ sẽ là : 0 0 iI i m n r n       . Trong bài tập này, tôi có thể đơn giản nhận ra giá trị t m i  sẽ được lựa chọn làm biến. Sau khi tôi đã có đủ hai thành phần quan trọng là bất biến vòng lặp I và biến chức năng i, nhiệm vụ tiếp theo tôi sẽ phải chứng minh lần lượt các điều kiện sau đây là đúng để khảng định tính đúng đắn của lệnh chu trình theo logic Hoare: ( 0 0 0 0) iI m n i m n r n           ( : 1; : 0) I 0r i I i m m i           : * ; : 1;I i m m i N r r n i i I m i N           mI i m r n    7 Bằng việc áp dụng các suy diễn logic tôi chứng minh đầy đủ những luận cứ để khảng định bộ ba Hoare là đúng. Do đó lệnh chu trình là đúng đắn.  : 1; : 0r i  while i m do  r : r*n;i : i 1;    mr n Từ hai bài tập trên, có lẽ phần nào tôi cũng đã nắm được cơ bản việc chứng minh tính đúng đắn của lệnh chu trình bằng phương pháp logic Hoare. CHƯƠNG 4. NGHIÊN CỨU VỀ BIẾN VÀ BẤT BIẾN TRONG PHƯƠNG PHÁP CHỨNG MINH TÍNH ĐÚNG ĐẮN CỦA LỆNH CHU TRÌNH Trong việc chứng minh, tôi nhận thấy muốn tìm ra một bất biến và biến đảm bảo đúng, đủ không phải là công việc dễ dàng. Thực tế, vấn đề này vẫn luôn đem lại một thách thức không hề nhỏ. Trong chương này, tôi sẽ cố gắng nghiên cứu các vấn đề liên quan đến bất biến và biến nhằm đem lại một cái nhìn đầy đủ về chúng đồng thời mong muốn tìm ra các phương pháp cụ thể xác định biến và bất biến trong vòng lặp. 4.1 Biến 4.1.1 Khái niệm Khái niệm biến (t) được phát biểu là một đại lượng có giá trị thay đổi trong mỗi lần thực hiện phần thân vòng lặp. Biến dùng để chứng minh tính dừng của vòng lặp. Tôi phải đảm bảo ban đầu (trước khi thực hiện phần thân) t phải có giá trị dương. 4.1.2 Phương pháp tìm biến Phương pháp đoán biến chức năng thường được sử dụng: - Lặp với một chỉ số, ở đây i được sử dụng là biến chỉ số của vòng lặp + N ± i là biến chức năng được chọn dễ dàng. + Áp dụng nếu bạn luôn luôn thêm hoặc luôn luôn trừ một hằng số, và nếu bạn thoát khỏi vòng lặp khi chỉ số đạt đến một số hằng số nào đó 8 + Sử dụng N-i nếu bạn đang tăng i, N + i nếu bạn được giảm giá trị của i + Thiết lập N với N ± i ≤ 0 ở lối ra vòng lặp, thường là bằng 0. Ví dụ: Tôi xét vòng lặp sau đây While (j < N) do s := s + a[j]; j := j + 1; End Với biến được xác định là t = N-j. Tôi có thể phân tích như sau: Khi j=N hiệu N-j sẽ nhận giá trị là 0, đồng nghĩa với việc vòng lặp kết thúc. Trong việc chứng minh tôi phải đảm bảo trường hợp biến (t, xem phần 3.1 và 3.2) ban đầu là dương nhằm thỏa mãn phần thân vòng lặp có thể được thực hiện. - Đối với các vòng lặp khác hãy tìm một biểu thức đó là một ràng buộc trên số lần lặp lại trong vòng lặp. Ví dụ: Xét bài toán tìm số lớn nhất của mảng A. i := a.lower ; j := a.upper While i ≠ j do If a[i] ≥ a[j] then j:= j -1 else i:= i + 1; Max:= a[i]; Tôi nhận thấy giá trị của i và j được thay đổi liên tục và có xu hướng kết thúc khi i= j. Vậy đơn giản tôi chọn được biến là t:= j – i. 4.2 Bất biến 4.2.1 Bất biến vòng lặp Mỗi vòng lặp, đặc biệt, phải có một bất biến vòng lặp. Mặc dù một số lập trình viên có thể tìm thấy bất biến như một việc đơn giản cần thiết chỉ để xác minh chính thức. Bất biến cung cấp thông tin cơ bản về vòng lặp, hiển thị những 9 gì nó đang cố gắng để đạt được và làm thế nào để đạt được nó. Do vậy tôi có thể nói là: tôi không thể hiểu được một vòng lặp mà không biết bất biến của nó. Các khái niệm về bất biến vòng lặp được thể hiện dễ dàng trong cú pháp vòng lặp sau đây: 1 from 2 Init 3 invariant 4 Inv 5 until 6 Exit 7 variant 8 Var 9 Loop 10 Body 11 end Mệnh đề biến chức năng (variant) giúp thiết lập chấm dứt vòng lặp, tôi sẽ tìm hiểu sau. Khởi tạo (Init) và thân vòng lặp (Body) là một danh sách các lệnh được thực hiện theo trình tự, một trong hai hoặc cả hai có thể là rỗng, mặc dù thực tế phần thân bình thường sẽ không rỗng. Exit (Điều kiện thoát) và Inv (bất biến) là biểu thức dạng logic vị từ trả ra kết quả là True hoặc False. Ngữ nghĩa của các vòng lặp là: (1) Thực thi Init. (2) Sau đó, nếu Exit có giá trị True, không làm gì cả; nếu nó có giá trị False, thực hiện Body, và lặp lại bước 2. Có rất nhiều biến thể của cấu trúc vòng lặp trong ngôn ngữ lập trình. Tất cả chúng đều có thể được bắt nguồn từ một hình thức cơ bản ở trên. Inv (bất biến vòng lặp) là một bất biến chính xác cho các vòng lặp, nếu có đủ các điều kiện sau đây: 10 (1) Mỗi thực hiện Init, bắt đầu ở trạng thái trước khi thực hiện vòng lặp, sẽ mang lại một trạng thái mà Inv nắm giữ. (2) Mỗi thực hiện Body, bắt đầu ở bất kỳ trạng thái nào mà Inv nắm giữ và Exit không nắm giữ (Có giá trị false), sẽ mang lại một trạng thái mà Inv nắm giữ một lần nữa. 4.2.2 Một cách nhìn mang tính xây dựng Hình 4. 1 . Các vòng lặp như là một sự tính toán bằng cắp xấp xỉ 4.2.3 Ví dụ cơ bản Để minh họa cho ý tưởng trên, tôi áp dụng trong thuật toán tìm ước chung lớn nhất của 2 số a và b. Thuật toán như sau: while a khác b do nếu a>b thì a:=a-b ngược lại b:=b-a; Uoc chung lon nhat la: a; Khi đó, Hậu điều kiện của thuật toán là: Result = UC(a, b) Trong trường hợp các số nguyên dương a và b là các đầu vào và UC là hàm toán học tính ước số chung lớn nhất. Tôi có thể viêt tổng quát như sau: Result = x  UC(Result, x) = UC(a,b) Với mỗi biến x mới, bằng các tính chất toán học, với mọi x, tôi có UC(x,x) = x 11 Những liên kết thứ hai, một sự tổng quát của hậu điều kiện, sẽ được sử dụng như là bất biến; các liên kết đầu tiên sẽ sử dụng như là điều kiện thoát vòng lặp. Để có được thân vòng lặp, áp dụng đặc tính phương pháp toán học tìm ước chung lớn nhất, tôi có: với mọi x> y thì UC (x, y) = UC (x-y, y) với mọi x< y thì UC (x, y) = UC (x, y-x) Tôi thể hiện thuật toán với bất biến vòng lặp như sau: 1 from 2 Result := a ; x := b 3 invariant 4 Result >0 5 x > 0 6 UC (Result, x) = UC (a, b) 7 until 8 Result = x 9 loop 10 if Result >x then 11 Result := Result − x 12 else /*Ở đây giá trị của x sẽ lớn hơn Result*/ 13 x := x − Result 14 end 15 variant 16 max (Result, x) 17 end Hình 4. 2. Ước số chung lớn nhất của hai số nguyên dương a và b 4.2.4 Phân loại bất biến: Bất biến vòng lặp có thể được chia theo hai hướng: o Bởi vai trò của nó đối với các hậu điều kiện, giúp tôi phân biệt giữa tính bất biến "cốt lõi" (“essential”) và "chặn" (“bounding”). 12 o Bằng các kỹ thuật chuyển đổi đó mang lại các bất biến từ hậu điều kiện. Ở đây tôi có kỹ thuật như tách cặp (uncoupling) và giảm dư hằng (constant relaxation). 4.2.4.1 Phân loại theo luật 4.2.4.2 Phân loại theo kỹ thuật khái quát hóa Giảm dư hằng: Tách cặp: 4.3 Tìm biến và bất biến trong một vài thuật toán cơ bản 4.3.1 Tìm phần tử có giá trị lớn nhất trong một dãy các phần tử 4.3.1.1 Số lớn nhất với vòng lặp một biến Kết quả được bất biến vòng lặp mong muốn là Result = max(a [ a. lower.. i] ) và a.lower ≤ i ≤ a.upper. Ở đây, tôi đã thay thế i=a.upper Tôi dễ ràng chọn ra được một biến chức năng là a.upper – i Hình 4.4 cho thấy việc thực hiện kết quả của thuật toán. 1 max_one_way (a: ARRAY [T]): T 2 require 3 a.count ≥ 1 /*a.count là số lượng phần tử của mảng*/ 4 local 5 i : INTEGER 6 do 7 from 8 i := a.lower ; Result := a [a.lower] 9 invariant 10 a.lower ≤ i ≤ a.upper 11 Result = max (a [a.lower, i]) 12 until 13 13 i = a.upper 14 loop 15 i := i + 1 16 if Result <a [i] then Result := a [i] end 17 variant 18 a.upper – i +1 19 end 20 ensure 21 Result = max (a) 22 end Hình 4. 3. Số lớn nhất với vòng lặp một biến 4.3.1.2 Số lớn nhất với vòng lặp hai biến 4.3.2 Tìm kiếm 4.3.2.1 Tìm kiếm trong một mảng chưa được sắp xếp 4.3.2.2 Tìm kiếm nhị phân 4.3.3 Sắp xếp 4.3.3.1 Sắp xếp chọn (Selection sort) 4.3.3.3 Sắp xếp kiểu nổi bọt (Bubble sort) 4.4 Ứng dụng kinh nghiệm tìm biến, bất biến trong một số bài tập. Từ tất cả những kiến thức và bài tập đã trình bày, tôi đã cố gắng tập hợp và nghiên cứu nhằm đưa ra những cái nhìn có hướng tổng quan nhất về biến và bất biến của vòng lặp. Sau đây tôi sẽ thử áp dụng những kiến thức có được để làm một số bài tập. Các bài tập được trình bày sau đây được trình bày theo logic đầu tiên là dự đoán biến và bất biến của vòng lặp, sau đó tôi chứng minh biến và bất biến được dự đoán là đúng. Bài 1. Cho chương trình (tựa mã) như sau: m := f [1]; p := 2; while p ≤ n do if f [p] < m then 14 begin m := f [p]; p := p + 1 end end Hãy xác định biến (t) và bất biến (I) đúng để chứng minh tính đúng đắn của chương trình. Bài giải: Tôi dự đoán biến và bất biến như sau : Biến : Tôi dự đoán một biến t = n – p + 1. Bất biến : Tôi dự đoán một bất biến của vòng lặp trên sẽ là:   min |1 1 2 1I m f i i p p n         . Công việc tiếp theo là chứng minh biến và bất biến tìm được là đúng : Biến : Chứng minh ban đầu t > 0 . 1 0p n n p     . Chứng minh sau mỗi lần thực hiện thân vòng lặp biến t phải giảm. Để thực hiện, tôi phải chứng minh vấn đề sau    b t N c t N   , đồng nghĩa với việc chứng minh Tôi phải làm rõ hai vấn đề sau + Thứ nhất:   1 ( ( 1) 1 )p n n p N f p m n p N            . + Thứ hai :     1 1p n n p N f p m n p N           . Bất biến: Để chứng minh I đúng tôi cần chứng minh thỏa mãn vấn đề sau    b I c I + Tôi làm rõ vấn đề thứ nhất:    P b c Q      min |1 1 2 1p n m f i i p p n f p m                 min |1 1 1 2 1 1f p f i i p p n           15 + Tôi làm rõ vấn đề thứ hai:  P b Q       min |1 1 2 1p n m f i i p p n f p m               min |1 1 2 1m f i i p p n         . Kết luận: Biến và bất biến tìm được là đúng. Tuy nhiên vòng lặp sẽ không dừng trong trường hợp gặp phải f [p] ≥ m. Bài 2. Cho chương trình (tựa mã) như sau: m := 0; p := 1; q := n; while p < q do if f (q) > f (p) then q := q – 1; else p := p + 1; m := f (p); Hãy xác định biến (t) và bất biến (I) đúng để chứng minh tính đúng đắn của chương trình. Bài giải: Tôi dự đoán biến và bất biến như sau Biến: Dạng này tôi dự đoán biến t = q – p. Bất biến: Tôi dự đoán một bất biến đó là:    1 { | } { | }min f i i n miI n f i p i q     . Chứng minh biến và bất biến đã dự đoán là đúng Biến Tôi phải chứng minh 0b t  , điều đó đồng nghĩa với việc chứng minh 0p q q p    . Chứng minh sau khi thực hiện thân vòng lặp biến phải giảm giá trị    b t N c t N   . Đối với chương trình này tôi phải chứng minh 16 Tôi cần chứng minh hai trường hợp sau Trường hợp f(q) > f(p) cho giá trị true: 1p q q p N q p N        . Trường hợp cho giá trị false: ( 1)p q q p N q p N        . Bất biến: Áp dụng luật rẽ nhánh tôi sẽ chứng minh như sau + Trường hợp 1: Tôi cần chỉ ra        1 { | } { | }p q min f i i n mi f q f pn f i p i q            1 1{ | } { | }min f i i n min f i p i q       . + Trường hợp 2: Tôi cần chỉ ra        1 { | } { | }p q min f i i n mi f q f pn f i p i q         Kết Luận: Bất biến và biến tôi dự đoán là đúng. Bài 3. Cho chương trình (tựa mã) như sau: Với m, i là các biến nguyên, n là một hằng nguyên dương. m := 0; i := 1; while i ≤ n do begin m := m + i*i; i := i + 1 end end Hãy xác định biến (t) và bất biến (I) đúng để chứng minh tính đúng đắn của chương trình. Giải: Tôi dự đoán biến và bất biến như sau Biến: Tôi dự đoán biến t = n – i +1. 17 Bất biến: Tôi chọn được một bất biến vòng lặp là 1 2 0 1 1 i j I i n m j         . Tới đây, tôi cần chứng minh biến và bất biến tìm được là đúng, như sau: Biến: Chứng minh đầu tiên t > 0. Để làm được điều đó tôi thực hiện chứng minh 0b t  đồng nghĩa với 1 0i n t n i      . Chứng minh    b t N c t N   ,  1 1 1i n n i N n i N          . Bất biến Tôi chứng minh bất biến sau khi thực hiện thân vòng lặp vẫn được bảo toàn. Với 1 2 0 1 1 i j I i n m j         . Tôi cần chứng minh Tôi phải cho thấy 1 1 1 2 2 2 0 1 1 1 1 1 1 i i j j i n i n m j i n m i j                      . Kết luận: Bất biến và biến tôi dự đoán là đúng. Bài 4. Cho chương trình (tựa mã) sau: Cho m, i là các biến nguyên, n là một hằng nguyên dương. m := 0; i := 1; while i ≤ n do begin if (i mod 2 = 0) then m := m + i ∗ i ∗ i; i := i + 1; end Hãy tìm biến (t) và bất biến (I) để chứng minh tính đúng đắn của chương trình. Giải: Tôi dự đoán biến và bất biến: 18 Biến: Tôi có biến t = n – i +1. Bất biến: Tôi được một bất biến như sau:    1 /2 3 0 1 1 2* i j I i n m j            . Chứng minh biến và bất biến tìm được là đúng: Biến : Đầu tiên tôi chứng minh t > 0. 0b t  đồng nghĩa với 1 0i n n i     . Tiếp theo tôi chứng minh sau khi thực hiện thân vòng lặp t phải giảm giá trị.    b t N c t N   đồng nghĩa với việc chứng minh 1 ( 1) 1i n n i N n i N          . Bất biến Tôi phải chứng minh hai trường hợp sau + Trường hợp 1 Tôi cần phải cho thấy    1 /2 3 0 1 1 2* ( mod2 0) i j i n i n m j i                         1 1 /2 33 0 1 1 1 2* i j i n m i j                      . + Trường hợp 2: Tôi cần phải cho thấy    1 /2 3 0 1 1 2* ( mod2 0) i j i n i n m j i                         1 1 /2 3 0 1 1 1 2* i j i n m j                     . Kết luận: Bất biến và biến tôi dự đoán là đúng. 19 Bài 5. Cho chương trình (tựa mã) sau: Cho m, i là các biến nguyên, n là một hằng nguyên dương. m := 0; i := 1; while i ≤ n do begin if (i mod 2 = 1) then m := m + i ∗ i ∗ i; i := i + 1; end Hãy tìm biến (t) và bất biến (I) để chứng minh tính đúng đắn của chương trình. Giải: Tôi dự đoán biến và bất biến: Biến: tôi có biến t = n – i +1. Bất biến: Tôi được một bất biến như sau:    2 /2 3 0 1 1 2* 1 i j I i n m j            Chứng minh biến và bất biến vừa tìm được là đúng: Biến: Với biến là t = n – i +1, tôi thực hiện chứng minh giống với bài tập 4. Kết luận biến t tìm được thỏa mãn yêu cầu. Bất biến Tôi phải chứng minh hai trường hợp sau + Trường hợp 1 Tôi cần phải cho thấy    2 /2 3 0 1 1 2* 1 ( mod 2 1) i j i n i n m j i                          1 2 /2 33 0 1 1 1 2* 1 i j i n m i j                       . + Trường hợp 2: 20 Tôi cần phải cho thấy    2 /2 3 0 1 1 2* 1 ( mod 2 1) i j i n i n m j i                          1 2 /2 3 0 1 1 1 2* 1 i j i n m j                      . Kết luận: Bất biến và biến tôi dự đoán là đúng. Bài 6. Cho chương trình (tựa mã) sau j:=1; k:=1; While j<n do j:= j + 1; k:= k * j; end Hãy tìm biến (t) và bất biến (I) để chứng minh tính đúng đắn của chương trình. Giải: Tôi dự đoán biến và bất biến cho chương trình trên Biến: Tôi dự đoán biến t = n – j. Bất biến: Tôi dự đoán bất biến của vòng lặp là 1 !I j n k j     . Chứng minh biến và bất biến là đúng Biến Đầu tiên tôi chứng minh biến ban đầu là dương, 0b t  đồng nghĩa với 0j n n j    . Tôi chứng minh    b t N c t N   đồng nghĩa với việc chứng minh:    : * ; : 1j n n j N k k j j j n j N         . Bất biến Tôi cần chứng minh    b I c I 21 Tôi phải cho thấy       1 ! 1 1 * 1 1 !j n k j j n k j j            . Kết luận: Bất biến và biến tôi dự đoán là đúng. Tôi nhận thấy vấn đề tìm biến và bất biến để chứng minh tính đúng đắn của lệnh chu trình thực sự không thể tìm được một phương pháp chung nhất. Vì cơ bản những bài toán khác nhau đề có hậu điều kiện và các ràng buộc khác nhau, điều đó mang lại sự đa dạng bất quy tắc. Để giải quyết được bài toán này chủ yếu dựa vào kinh nghiệm trong việc áp dụng một vài gợi ý đã trình bày trong chương IV. CHƯƠNG 5. KẾT LUẬN 5.1 Kết luận Các kết quả nghiên cứu về đề tài chứng minh tính đúng đắn của chu trình bằng logic Hoare không phải là mới nhưng thực sự nó vẫn còn mang tính thời sự rất cao. Việc áp dụng vào thực tế trong việc chứng minh tính đúng của chương trình góp phần quan trọng để đảm bảo một chương trình thỏa mãn yêu cầu lập trình. Trong phần luận văn tôi đã cố gắng dẫn dắt những kiến thức theo một logic hợp lý và trực quan nhất. Những lý thuyết cơ bản và bài tập ví dụ được đưa ra xen kẽ và liên tục (từ chương 2 đến chương 4) với mục đích không chỉ là cung cấp lý thuyết mà còn đem lại cho bản thân cũng như người đọc một vài kinh nghiệm rút ra trong việc tìm biến và bất biến để chứng minh tính đúng đắn của chu trình. Những kiến thức của phần luận văn có thể được tổng hợp một cách vắn tắt như sau: Đầu tiên là những kiến thức tổng quan về logic vị từ, logic Hoare; Các kỹ thuật chứng minh tính đúng của lệnh chu trình bằng phương pháp logic Hoare kèm vào đó là các ví dụ minh họa chi tiết cho việc chứng minh; Làm rõ 22 hơn về biến và bất biến, đi xâu vào tìm hiểu về bất biến vòng lặp, các ví dụ minh họa được thể hiện trên một vài thuật toán cơ bản nhất; Cuối cùng các kinh nghiệm rút ra từ việc nghiên cứu trong quá trình thực hiện tìm biến, bất biến trên các ví dụ vòng lặp cụ thể. Trên thực tế có nhiều công cụ tự động trong việc chứng minh tính đúng đắn của chương trình, tuy nhiên hiểu rõ phương pháp chứng minh, hiểu rõ bản chất của vòng lặp luôn làm cho người lập trình ít mắc sai sót trong quá trình viết code. Khi đó, chương trình được viết ra sẽ đảm bảo chạy đúng và ổn định hơn. Giảm thiểu rủi ro và kinh phí. Qua quá trình nghiên cứu về luận văn, bản thân tôi đã lĩnh hội được một lượng kiến thức khá lớn từ đó đã làm rõ những ưu tư, thắc mắc của mình trong quá trình giảng dạy bộ môn tin học tại cấp độ THPT. Đó là những kiến thức liên quan đến tính đúng đắn của chương trình, đến bản chất của vòng lặp, đến tính kết thúcThực sự rất là hữu ích trong việc giảng dạy học sinh lớp 10 (trong các bài liên quan đến thuật toán), học sinh lớp 11 (giảng dạy về ngôn ngữ lập trình, Pascal). 5.2 Hạn chế và kiến nghị Sau khi nghiên cứu, tôi đã cố gắng tổng hợp, phân tích các tài liệu liên quan đến luận văn, tham khảo ý kiến hướng dẫn của TS. Đặng Văn Hưng nhằm mục đích tìm ra một phương pháp giải cơ bản nhất cho bài toán tìm biến và bất biến cho việc sử dụng logic Hoare để chứng minh tính đúng đắn. Tuy nhiên, sẽ chẳng có một phương pháp hay một lời giải nào chung nhất và tốt nhất. Cơ bản phần nhiều nó dựa trên những kinh nghiệm có được trong quá trình tìm kiếm. Chắc chắn rằng với trình độ hạn hẹp của bản thân và trong thời gian nghiên cứu làm luận văn, công việc dạy học cộng thêm đó là việc gia đình con nhỏ làm cho bản thân thực sự chưa hoàn thành được luận văn ở mức độ cao nhất mong muốn. Luận văn được viết ra sẽ còn nhiều những mặt hạn chế, sai sót. Vậy, tôi rất mong nhận được sự quan tâm, đồng cảm và đóng góp ý kiến từ phía thầy cô, bạn bè để luận văn được hoàn thiện hơn. 23 TÀI LIỆU THAM KHẢO Tiếng Việt [1] Đỗ Đức Giáo (2011), Toán rời rạc ứng dụng trong tin học, Nhà xuất bản giáo dục Việt Nam. [2] Lê Văn Viễ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, Báo cáo tốt nghiệp. [3] Zoharn Manna, Người dịch TS. Đặng Văn Hưng, Lô Gích về lập trình, Trung tâm toán máy tính. Tiếng Anh [4] Jonathan Aldrich, 17-654/17-765 Analysis of Software Artifacts. [5] C.A.R. Hoare, An Axiomatic Basis for Computer Programming, The Queen’s University of Belfast, *Northern Ireland. [6] Dang Van Hung, Formal Methods An Introduction, College of Technology. [7] CARLO A. FURIA, ETH Zurich, BERTRAND MEYER, Loop invariants: analysis, classification, and examples, ITMO St. Petersburg, and Eiffel Software, SERGEY VELDER. [8] Ichiro Hasuo, Tutorial on Formal Verification using Hoare Logic, Dept. Computer Science, University of Tokyo. [9] Anders Møller, Program Verification with Hoare Logic, university of Aarhus.