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

trình bày ở trên trong quá trình vòng lặp là nó làm nổi bật bản chất của bất biến: Nó là một dạng tổng quát của hậu điều kiện mong muốn, mà trong một trường hợp đặc biệt (đại diện bởi các điều kiện thoát vòng lặp) sẽ cho tôi hậu điều kiện đó. Quan điểm này của bất biến, như là một cách đặc biệt trong khái quát các mục tiêu mong muốn của việc tính toán vòng lặp, giải thích lý do tại sao bất biến vòng lặp là một tài sản quan trọng như vậy của các vòng lặp; ai có thể tranh luận rằng sự hiểu biết một vòng lặp có nghĩa là sự hiểu biết bất biến của nó (mặc dù các quan sát rõ ràng rằng nhiều người lập trình viết các vòng lặp mà gần như chưa bao giờ chính thức học qua khái niệm bất biến, mặc dù tôi có thể khẳng định rằng nếu họ hiểu những gì họ đang làm họ đang dựa vào một số hiểu biết trực giác về bất biến, như ông Jourdain Moli`ere đã nói). 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ố nguyên dương 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 bài 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 29 Do vậy, tôi có được các thành phần của bất biến là: Result >0 và x > 0 UC (Result, x) = UC (a, b) 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 o Các bất biến cần thiết là bất biến bảo toàn. Nó thể hiện rằng một số lượng nhất định vẫn còn tương đương với giá trị ban đầu của nó. o Các chiến lược dẫn đến bất biến bảo toàn này là tách cặp, thay thế thuộc tính của một biến (Result), được sử dụng trong các hậu điều kiện, bằng một thuộc tính của hai biến (Result và x), được sử dụng trong bất biến. 30 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”). 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 Trong chiến lược lặp điển hình được mô tả trong phần 4.1.2, vấn đề cần thiết đó là việc lặp đi lặp lại liên tiếp của thân vòng lặp duy trì trong các vùng hội tụ nơi dạng thức tổng quát của hậu điều kiện được xác định. Các điều kiện tương ứng, tạo nên bất biến chặn; các mệnh đề mô tả hậu điều kiện tổng quát là bất biến cốt lõi. Các bất biến chặn áp dụng cho thuật toán tìm ước số chung lớn nhất bao gồm các mệnh đề: Result > 0 x > 0 Mệnh đề quan trọng là: UC(Result, x) = UC(a, b) Cho kết quả hậu điều kiện nếu Result = x. Đối với các chương trình tìm số lớn nhất trong mảng một chiều, bất biến chặn là: a.lower ≤ i ≤ a.upper và bất biến cốt lõi là: Result = max (a [a.lower.. i] ) Cho kết quả hậu điều kiện khi i = a.upper. Lưu ý rằng bất biến cốt lõi sẽ không được định nghĩa nếu không có bất biến chặn, vì a [1 .. i] sẽ chưa được xác định (nếu i> a.upper) hoặc sẽ là trống rỗng và không lớn nhất (nếu i <a.lower ). Đối với các chương trình tối đa hai chiều, bất biến chặn là: a.lower ≤ i ≤ j ≤ a.upper và bất biến cốt lõi là: max(a) = max(a[i..j]) Cho kết quả các hậu khi i = j. Một lần nữa, bất biến cốt lõi sẽ không luôn luôn được xác định mà không có bất biến chặn. 31 Việc tách biệt giữa bất biến chặn và bất biến cốt lõi thường là đơn giản như trong các ví dụ. Trong trường hợp nghi ngờ, các quan sát sau đây sẽ giúp phân biệt. Các chức năng tham gia vào bất biến thường là một phần; ví dụ: o UC (u, v) được xác định nếu u và v đều khác không (và, vì tôi xem xét các số nguyên tự nhiên duy nhất trong ví dụ, tích cực). o Đối với mảng a và một số nguyên i, a [i] được xác định nếu  . .. .i a lower a upper và a [i .. j] là khác rỗng chỉ khi    .. . .. .i j a lower a upper . o Max (a) được chỉ định nếu các mảng a là không trống rỗng. 4.2.4.2 Phân loại theo kỹ thuật khái quát hóa Các bất biến cốt lõi là một đột biến (thường là một sự suy yếu) của hậu điều kiện vòng lặp. Các kỹ thuật đột biến sau đây là đặc biệt phổ biến: Giảm dư hằng: thay thế một hằng số n (thường hơn, một biểu hiện mà không thay đổi trong quá trình thực hiện các thuật toán) bằng một biến i, và sử dụng i = n như là một phần hoặc tất cả các điều kiện thoát. Giảm dư hằng là kỹ thuật được sử dụng trong việc tính toán giá trị lớn nhất của mảng một chiều, nơi hằng số là giới hạn trên của mảng. Các bất biến khái quát các hậu điều kiện "Result là lớn nhất của mảng cho tới a.lower", nơi a.lower là một hằng số, "Result là lớn nhất cho tới i". Điều kiện này là tầm thường để cho những thiết lập ban đầu của một mảng không rỗng (lấy i thay thế a.lower), dễ dàng mở rộng để tăng giá trị của i lên (lấy Result là lớn hơn giá trị trước đó của nó và a [i]), và kết quả là hậu điều kiện khi i đạt đến a. upper. Tìm kiếm nhị phân khác với tìm kiếm tuần tự bằng cách áp dụng giảm dư hằng, cho cả các giới hạn trên và dưới của mảng. Trong phần 3.2 các ví dụ chứng minh, tôi cũng đã áp dụng kỹ thuật giảm dư hằng trong công việc tìm bất biến vòng lặp. Đối với bài toán 1, hậu điều kiện là 1 n j Q s j          với n là hằng số giới hạn trên của khoản giá trị của biến chỉ số vòng lặp. Khi đó việc thay thế n bằng biến i là một tính toán dễ hiểu nhằm làm cho hậu điều kiện phụ thuộc vào chỉ số của vòng lặp. Bằng một vài tính toán khác nhằm phù hợp với bài toán tôi có được bất biến như mong muốn. Bài toán thứ 2, hậu điều kiện là  mr n việc thay thế hằng số m cũng được thực hiện tương tự bằng một biến chỉ số vòng lặp là i. Tôi dễ dàng có được một bất biến cốt lõi của vòng lặp là  ir n . 32 Tách cặp: thay thế một biến v (thường Result) bằng hai (trong ví dụ phần 4.1.3 là result và x), sử dụng bình đẳng của chúng như là một phần hoặc là tất cả đối với các điều kiện thoát vòng lặp. Tách cặp được sử dụng trong thuật toán ước số chung lớn nhất. 4.3 Tìm biến và bất biến vòng lặp 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 Phương pháp max_one_way trả về phần tử tối đa của mảng a (mảng chưa được sắp xếp) trong giới hạn giữa a.lower và a.upper. Giá trị lớn nhất chỉ được xác định áp dụng đối với một mảng có ít nhất một phần tử, do đó các điều kiện tiên quyết . 1a count  . Chương trình cơ bản như sau của thuật toán: Result:=a[a.lower]; i:=a.lower; while i<a.upper do begin i:=i+1; if Result < a[i] then Result:= a[i]; end; Các hậu điều kiện có thể được viết là: Result = max(a) Viết nó ở dạng phần tử mảng, tôi có Result = max (a [a.lower..a.upper]) cho tôi kết quả bất biến của giảm dư hằng trong giới hạn giữa a.lower và a.upper. Tôi chọn một trong hai để thay thế, 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 Việc tìm biến được thực hiện như sau: Nhận thấy chỉ số của vòng lặp thay đổi trong khoảng giới hạn giữa a.lower và a.upper. Giá trị của i được khởi tạo bắt đầu bằng a.lower, nó liên tục tăng lên đến khi i = a.upper vòng lặp sẽ dừng lại. Giá trị của biến sẽ thay đổi liên tục, qua phân tích ở trên tôi dễ ràng chọn ra được một biến chức năng là a.upper – i , bởi vì với i = a.upper thì a.upper – i = 0 do đó vòng lặp sẽ kết thúc. Khi i 0 đảm bảo phần thân vòng lặp được thực hiện. 33 Hình 4.3 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 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 Thuật toán số lớn nhất với vòng lặp một biến lựa chọn độc đáo để áp dụng giảm dư hằng là a.lower hoặc (như trong thuật toán phần 4.3.1.1 ở trên) là a.upper. Đối với thuật toán số lớn nhất với vòng lặp hai biến tôi hướng tới một mối quan tâm có tính đối xứng. Tôi có thể chọn một cặp giảm dư hằng. Nếu i và j là hai biến số giảm dư, thân vòng lặp hoặc tăng i, hoặc giảm j. Khi i = j, vòng lặp đã xử lý tất cả các phần tử của mảng a, và vì thế i hoặc j là biến chỉ số cho tôi biết phần tử lớn nhất. Hậu điều kiện có thể được viết là: Result = max(a) 34 Tôi viết nó dưới dạng phần tử mảng Result = max (a [a.lower..a.upper]). Khi được thay thế cặp giảm dư hằng i := a.lower và j := a.upper, tôi được max (a [i..j]). Khi đó tôi chọn được bất biến vòng lặp mong muốn là a.lower ≤ i ≤ j ≤ a.upper và max (a [i..j]) = max (a). Biến được xác định bằng hiệu của hai cặp giảm dư hằng là i – j. Thực vậy khi i = j. Hiệu số sẽ bằng 0 và khi đó vòng lặp sẽ kết thúc. Các đặc tả kỹ thuật (điều kiện tiên quyết và hậu điều kiện) cũng giống như đối với các thuật toán với vòng lặp một biến. Hình 4.4 cho thấy việc thực hiện thuật toán như sau: 1 max_two_way (a: ARRAY [T]): T 2 require 3 a.count ≥ 1 4 local 5 i , j: INTEGER 6 do 7 from 8 i := a.lower ; j := a.upper 9 invariant 10 a.lower ≤ i ≤ j ≤ a.upper 11 max (a [i..j]) = max (a) 12 until 13 i = j 14 loop 15 if a [ i ] > a [ j] then j := j − 1 else i := i + 1 end 16 variant 17 j − i 18 end 19 Result := a [i] 20 ensure 21 Result = max (a) 22 end Hình 4. 4. Số lớn nhất với vòng lặp hai biến. 35 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 Chương trình has_sequential sau đây trả ra vị trí xuất hiện của một phần tử khóa (key) trong một mảng a hoặc, nếu key không xuất hiện, sẽ trả ra một giá trị đặc biệt. Thuật toán áp dụng đối với bất kỳ cấu trúc tuần tự nào nhưng được sử dụng ở đây là cho cấu trúc mảng. Để đơn giản, tôi giả định rằng a.lower (cận dưới của mảng) là 1, với mục đích tôi có thể chọn 0 như là một giá trị đặc biệt. Các đặc điểm kỹ thuật có thể sử dụng các yếu tố ký hiệu miền elements (a) để diễn tả tập các phần tử của một mảng a. Một dạng thức đơn giản của hậu điều kiện là 0 (a)Result key elements   (10) Mà chỉ cần ghi lại xem key đã được tìm thấy. Thay vào đó, tôi sẽ sử dụng một dạng thức có thể ghi lại vị trí các phần tử xuất hiện nếu có: 0 a(Result)Result key   (11) 0 (a)Result key elements   (12) Để cho rõ ràng tôi thêm vào trước các điều khoản ràng buộc  0.. .Result a upper Để làm cho nó rõ ràng rằng các truy cập mảng trong (11) được xác định khi cần thiết. Nếu trong (12) tôi thay thế mảng a bởi  1.. .a a upper , tôi có được bất biến của vòng lặp tìm kiếm tuần tự bằng cách giảm dư hằng: giới thiệu một biến i để thay thế một trong các giới hạn 1 và a.upper. Tôi có được những thành phần của bất biến sau đây: 0 ≤ i ≤ a.count  0,iResult  0Result key a Result     0 1..Result key elements a i   Biến chức năng được xác định như sau: Các phân tích trên cho thấy tăng i liên tục, bắt đầu từ 0 tiến dần tới a.count. Khi i= a.upper vòng lặp sẽ chấm dứt. Tôi đơn giản nhận ra rằng biến được chọn là: t = a.upper – i+1. 1 has sequential (a: ARRAY [T]; key: T): INTEGER 2 require 36 3 a.lower = 1 4 local 5 i: INTEGER 6 do 7 from 8 i := 0 ; Result := 0 9 invariant 10 0 ≤ i ≤ a.count 11  0,iResult 12  0Result key a Result   13   0 1..Result key elements a i   14 until 15 i = a.upper 16 loop 17 i := i + 1 18 if a [i] = key then Result := i end 19 variant 20 a.upper − i + 1 21 end 22 ensure 23  0,a.upperResult 24  0Result key a Result   25  0Result key elements a   26 end Hình 4.5. 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 Tìm kiếm nhị phân hoạt động trên các mảng đã được sắp xếp bằng việc lặp đi lặp lại giảm một nửa, một phân đoạn của mảng đó. Tìm kiếm sẽ kết thúc, hoặc khi phần tử key được tìm thấy hoặc khi phân khúc này trở nên trống rỗng, ngụ ý rằng các phần tử không xuất hiện ở một nơi nào trong mảng. 37 Mặc dù ý tưởng cơ bản của tìm kiếm nhị phân là tương đối đơn giản, nhưng khi thực hiện các chi tiết có thể gây ngạc nhiên vì sự khó khăn, và nhiều người lập trình đã làm sai trong vài lần đầu tiên họ cố gắng. Lý luận một cách cẩn thận trên các đặc điểm kỹ thuật (ở cấp lý thuyến miền) và kết quả bất biến nhằm giúp tránh mắc phải những sai lầm. Tôi thấy các hậu điều kiện cũng giống như đối với tìm kiếm tuần tự (mục 4.1.3). Thuật toán và thực hiện bây giờ có điều kiện tiên quyết sorted (a) Sử dụng lý thuyết miền Sorted (a), được định nghĩa là      . ow .. . 1 : 1j a l er a upper a j a j     Định lý miền mà trên đó tìm kiếm nhị phân dựa vào là, đối với bất kỳ giá trị mid nằm trong khoảng [i .. j] (nơi mà i và j là chỉ số giá trị của mảng), và một giá trị key bất kỳ kiểu T (kiểu của các phần tử mảng) :   ..key elements a i j              .. 1.. key a mid key elements a i mid key a mid key elements a mid j                (13) Công thức (13) không đối xứng đối với i và j; một phiên bản đối xứng là khả thi, sử dụng trong các phân đoạn, "≥" hơn là ">" và mid hơn là mid + 1. Các mẫu ở (13) có lợi thế của việc sử dụng hai điều kiện loại trừ lẫn nhau trong so sánh các key với a [mid]. Kết quả là, tôi có thể giới hạn trong mảng a giá trị mid được chọn trong [i .. j - 1] (chứ không phải là [i .. j]) từ phân đoạn đầu tiên không liên quan j và các phân đoạn thứ hai có thể không giữ cho mid = j ( a [mid + 1..j] sau đó rỗng). Tất cả những quan sát và lựa chọn ra những kết quả trực tiếp trên văn bản chương trình, nhưng được xử lý tốt hơn các mức đặc điểm kỹ thuật (lý thuyết). Tôi sẽ bắt đầu cho sự đơn giản với phiên bản (10) của hậu điều kiện mà chỉ ghi key xuất hiện hay không xuất hiện, lặp đi lặp lại ở đây để dễ tham khảo: 0 (a)Result key elements   (14) Nhân đôi phía bên tay phải của (14), viết a trong lát tạo thành a [1 .. a.upper], và áp dụng giảm dư hằng hai lần, đến hạn dưới 1 và giới hạn trên a.upper, các thuộc tính của bất biến bất biến cần thiết: 38    (a .. )key elements i j key elements a   (15) Với bất biến chặn 1 .i mid j a upper    Trong đó kết hợp các giả định trên mid cần thiết để áp dụng (13) - cũng thừa nhận trong (15) - và các kiến thức bổ sung 1 i và .j a upper . Cốt lõi của phần trình bày này là: - Hai mệnh đề key ≤ a [mid] và key> a [mid] của (13) là những điều kiện bổ sung dễ kiểm tra, cho thấy một thân vòng lặp bảo tồn bất biến bằng cách kiểm tra key đối với a [mid] và đi sang trái hoặc phải như là kết quả của việc kiểm tra. - Khi i = j, trường hợp phục vụ như là điều kiện thoát, phía bên trái của sự tương đương (15) giảm đến key = a [mid]; Đánh giá biểu thức này cho tôi biết liệu key đã xuất hiện ở tất cả trong toàn bộ mảng, các thông tin tôi tìm kiếm. Ngoài ra, tôi có thể có được hậu điều kiện mạnh mẽ hơn, (11) - (12), trong đó cung cấp Result giá trị chính xác, bởi đơn giản là gán chỉ số mid với Result. Những điều trên đây được thể hiện trong thuật toán hình 4.6: 1 has binary (a: ARRAY [T]; key: T): INTEGER 2 require 3 a.lower = 1 /*Để thuận tiện, xem phần phân tích tìm kiếm tuần tự.*/ 4 a.count > 0 5 sorted (a) 6 local 7 i , j, mid: INTEGER 8 do 9 from 10 i:= 1; j := a.upper; mid :=0; Result := 0 11 invariant 12 1 ≤ i ≤ mid≤ j ≤ a.upper 13    (a .. )key elements i j key elements a   14 until 15 i = j 16 loop 17 mid := i + (j − i)//2 18 if a [mid] < key then i := mid +1 else j := mid end 39 19 variant 20 j − i 21 end 22 if a [mid] = key then Result := mid end 23 ensure 24 0 Result n  25 0Result key a Result     26  0Result key elements a   27 end Hình 4. 6. Tìm kiếm nhị phân 4.3.3 Sắp xếp Một số thuật toán quan trọng sắp xếp một mảng dựa trên so sánh cặp và hoán đổi các phần tử. Các ký hiệu miền thuyết sau đây sẽ hữu ích cho mảng a và b: - Perm (a, b) thể hiện rằng mảng là một hoán vị của nhau (các tính chất của chúng đều giống nhau). - Sorted (a) thể hiện rằng các phần tử mảng xuất hiện trong thứ tự tăng dần:      . ow .. . 1 : 1i a l er a upper a i a i     . Các thuật toán sắp mảng ở đây, có các đặc điểm kỹ thuật: sort (a: ARRAY [T]) require a.lower = 1 a.count = n ≥ 1 ensure perm (a, old a) sorted (a) Bài toán sắp xếp kiểu nổi bọt (Bubble sort) Là một phương pháp sắp xếp khá phổ biến, Bubble sort được biết đến không phải là do hiệu quả làm việc của nó mà chỉ bởi vì nó đơn giản. Nó dựa trên ý tưởng của sự đảo ngược: một cặp phần tử chưa được sắp xếp sẽ được đảo ngược 40 thành một cặp phần tử được sắp xếp nếu mà phần tử đầu tiên lớn hơn phần tử thứ hai. Các quan sát đơn giản cho tôi thấy một mảng được sắp xếp nếu và chỉ nếu nó không còn có sự đảo ngược. Điều đó đưa đến gợi ý để sắp xếp một mảng bằng cách lặp đi lặp lại việc loại bỏ tất cả các hoán đổi. Bất biến trong trường hợp này được rút ra từ hậu điều kiện (Điều đó giống như các thuật toán sắp xếp khác). Hậu điều kiện perm(a, old a) với các yếu tố không thay đổi, cũng là một bất biến của hai vòng lặp lồng nhau được sử dụng trong Bubble sort. Các hậu điều kiện khác sorted(a) được thay vì suy yếu, nhưng theo một cách khác nhau hơn so với các thuật toán sắp xếp khác trước đó. Tôi giới thiệu một cờ swapped kiểu Boolean, trong đó ghi lại nếu có một số đảo ngược đã được gỡ bỏ bằng cách hoán đổi một cặp phần tử. Khi swapped là false sau khi quét toàn bộ các phần tử của mảng a, không có đảo đã được tìm thấy, và do đó a đã được sắp xếp. Do đó, tôi sử dụng ws apped như điều kiện thoát của các vòng lặp chính. Hậu điều kiện  w ors apped s ted a  (16) Là bất biến vòng lặp cốt lõi của thuật toán. Các vòng lặp bên thực hiện việc quét mảng đầu vào so sánh tất cả các cặp phần tử liền kề sau đó hoán đổi chúng khi chúng có đảo ngược. Thực hiện việc quét tiến tuyến tính từ phần tử đầu tiên đến người cuối cùng, tôi có được một bất biến cần thiết cho vòng lặp bên trong bằng cách thay thế n bởi i trong (16) viết bằng dạng slice:  w 1..s apped sorted a i    (17) Bất biến chặn 1 ≤ i ≤ n và bất biến vòng ngoài là mệnh đề perm(a, old a) hoàn thành bất biến vòng lặp bên trong. Được thể hiện trong thuật toán (hình 4.7). Các vòng lặp bên trong, đặc biệt, thiết lập swapped thành True bất cứ khi nào nó tìm thấy một số đảo ngược trong khi quét. Điều này báo hiệu rằng việc quét các phần tử của mảng là cần thiết trước khi mảng chắc chắn được sắp xếp. Xác minh tính đúng đắn của chương trình chú thích trong hình 4.7 là dễ dàng, bởi vì bất biến vòng lặp cốt lõi (16) và (17) là hiển nhiên đúng trong tất cả các lần lặp lại nơi swapped được thiết lập là True. Tôi nhận thấy, vòng lặp thực sự kết thúc khi chỉ số của mảng tăng lên đến n, đồng nghĩa với việc quét hết các phần tử của mảng, điều đó được thực hiện trong vòng lặp trong. Khi đó tôi chọn được một biến đối với vòng lặp trong là: n- i, giá trị của hiệu số sẽ về 0 khi i chạy đến n. Đối với vòng lặp ngoài, khi không còn sự hoán đổi nào được tìm thấy vòng lặp sẽ chấm dứt. 41 1 bubble sort basic (a: ARRAY [T]) 2 require 3 a.lower = 1 ; a.count = n ≥ 1 4 local 5 swapped: BOOLEAN 6 i : INTEGER 7 do 8 from swapped := True 9 invariant 10 perm (a, old a) 11  w ors apped s ted a  12 until ws apped 13 loop 14 swapped := False 15 from i := 1 16 invariant 17 1 ≤ i ≤ n 18 perm (a, old a) 19   w or 1..s apped s ted a i  20 until i = n 21 loop 22 if a [ i ] > a [ i + 1] then 23 a.swap (i, i + 1) *Hoán đổi các phần tử ở vị trí i và i+1*/ 24 swapped := True 25 end 26 i := i + 1 27 variant n − i end 28 variant |inversions (a) | 29 end 30 ensure 31 perm (a, old a) 32 sorted (a) 33 end Hình 4. 7. Sắp xếp kiểu nổi bọt. 42 4.4 Ứng dụng kinh nghiệm để tìm biến, bất biến trong một số bài toán. Từ tất cả những kiến thức và bài toán đã trình bày, tôi đã cố gắng tập hợp phân tích 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 toán. Các bài toán đượ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ã) 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 nhận ra biến chỉ số của vòng lặp là j. Trường hợp này trong điều kiện lặp chỉ với một chỉ số. Giá trị của j thay đổi trong khoảng 1 j n  , Khi j = n vòng lặp sẽ kết thúc. Tôi dự đoán biến t = n – j. Bất biến: Đây là đoạn chương trình tính n!. Hậu điều kiện tổng quát của chương trình là k = n!. Áp dụng kỹ thuật giảm dư hằng tôi thay n bằng biến chỉ số của vòng lặp là j. Khi đó tôi được bất biến cốt lõi là k = j!. Với bất biến chặn là 1 j 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    . Điều này được kiểm chứng bằng những logic sau: j n Giả thiết 43 0n j  Chuyển vế Tôi 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   đồng nghĩa với việc chứng minh:  j n n j N      1n j N   : * ;k k j   1n j N   : 1j j   n j N  Nhiệm vụ của tôi cần chỉ ra rằng ( 1)j n n j N n j N        . Điều đó được minh chứng bằng những logic sau: n j N  Giả thiết 1n j N   Định nghĩa phép < ( 1)n j N   Quy luật toán học Bất biến Tôi chứng minh sau khi thực hiện thân vòng lặp bất biến được bảo toàn. Với bất biến 1 !I j n k j     , tôi cần chứng minh    b I c I tương đương với việc chứng minh thỏa mãn: {1 !j n k j j n      }  1 1 *( 1) ( 1)!j n k j j       j:=j+1;  1 * !j n k j j    k:=k*j; {1 !j n k j    } Tôi phải cho thấy       1 ! 1 1 * 1 1 !j n k j j n k j j            . Được kiểm chứng bằng những logic sau: 1 1j  Vì 1 j 1j n  Vì j n  *( 1) !* 1k j j j   Vì theo giả thiết !k j b t N  Luật ghép Luật gán t N b I Luật phép gán, ghép Luật phép gán I 44 Kết luận: Bất biến và biến tôi dự đoán là đúng. Bài 2. Cho chương trình (tựa mã) như sau: m := f (1); p := 2; while p ≤ n do if f (p) < m then 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 nhận thấy đây là vòng lặp thực hiện lặp với một chỉ số trong điều kiện lặp, chỉ số lặp p sẽ tăng lên đến n. Vòng lặp kết thúc khi p vượt quá n. Theo kinh nghiệm đã trình bày ở phần 4.1.2 tôi dự đoán một biến t = n – p + 1. Việc cộng thêm 1 vào hiệu n – p cho tôi một đảm bảo biến t không âm vì p có giá trị lớn nhất là n+1. Ở đầu ra của vòng lặp t = 0. Bất biến : Đoạn mã trên thực hiện bài toán tìm số nhỏ nhất trong một dãy các số có thứ tự từ 1 đến n. Hậu điều kiện tổng quát của chương trình sẽ là “m = min {f(i) | 1 ≤ i ≤ n }”. Sử dụng kỹ thuật giảm dư hằng nhằm mục đích cho bất biến phụ thuộc vào chỉ số lặp của vòng lặp. Khi đó, tôi thay thế n bằng p điều đó cho tôi dự đoán một bất biến của vòng lặp trên sẽ là:   min |1 1 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 . Theo logic Hoare tôi phải chứng minh 0I b t   đồng nghĩa với 1 0p n n p     . Tôi sẽ chứng minh như sau : p n Theo giả thiết 0n p  Chuyển vế p 1 1n p   Cộng 2 vế với 1 45 1 0n p   Tính chất của phép so sánh. 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            1 ( 1) 1 : ( 1) 1 : 1 1 p n n p N f p m n p N m f p n p N p p n p N                      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            . Được minh chứng bằng những logic sau 1n p N   Giả thiết 1 1n p N    Định nghĩa phép <  1 1n p N    Quy tắc toán học. + Thứ hai :     1 1p n n p N f p m n p N           . Tôi không thể xác minh được hay nói cách khác là sai. Từ điều này dẫn đến kết luận vòng lặp này sẽ không dừng trong trường hợp chỉ số p không được thỏa mãn để tăng. 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 Điều đó tương đương với việc chứng minh      min |1 1 1p n m f i i p p n f p m                min |1 1 1 1 1f p f i i p p n          :m f p    min |1 1 1 1 1m f i i p p n         b I Luật phép gán, tuần tự. Luật phép gán 46 : 1p p     min |1 1 1m f i i p p n       + 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           Điều này được minh chứng bằng những logic sau 2 1p  2 p 1 1p n   Vì p n   min |1 1m f i i p    Giả thiết        min min |1 1 ,f p f i i p f p    Bởi vì        min |1 1 1 min |1 1 ,f i i p f i i p f p              min m,f p f p f p  Vì  f p m + 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         . Điều này hiển nhiên đúng. 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 3. 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); I 47 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 Chú ý vào điều kiện của vòng lặp tôi thấy hai biến chỉ số là p và q đều có thể được thay đổi giá trị. Chỉ số p tăng lên và q giảm dần giá trị. Vòng lặp kết thúc khi p = q. Dạng này tôi dự đoán biến t = q – p. Hiệu q – p = 0, đồng nghĩa với vòng lặp kết thúc khi p = q. Bất biến: Chương trình này dùng để tìm số nhỏ nhất của dãy số. Hậu điều kiện tổng quát của chương trình là “m = min {f(i) | 1 ≤ i ≤ n }”. Sử dụng kỹ thuật giảm dư hằng, tôi dùng một cặp biến chỉ số của vòng lặp là p và q. Với 1 ≤ p≤q ≤ 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 Chứng minh đầu tiên biến phải dương, t > 0. 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    . Thỏa mãn bằng những logic sau p q Giả thiết 0q p  Chuyển vế 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  p q q p N        : –1 f p f q q q   if then Tôi cần chứng minh hai trường hợp sau   : 1; q p p N p    else 48 Trường hợp f(q) > f(p) cho giá trị true: 1p q q p N q p N        . Điều đó được kiểm chứng bằng những logic sau q p N  Giả thiết 1 1q p N    Trừ cả 2 vế cho 1 1q p N   Định nghĩa phép < Trường hợp cho giá trị false: ( 1)p q q p N q p N        . Điều đó được kiểm chứng bằng những logic sau q p N  Giả thiết 1 1q p N    Trừ cả 2 vế cho 1 1q p N   Định nghĩa phép < ( 1)q p N   Quy luật toán học Bất biến: Áp dụng luật rẽ nhánh tôi sẽ chứng minh như sau Với bất biến dự đoán là    1 { | } { | }min f i i n miI n f i p i q        { | } { | }1 p q min f i i n min f i p i q       if f (q) > f (p) then    1 1{ | } { | }min f i i n min f i p i q      q := q – 1; else    1 { | } +1 { | } min f i i n min f i p i q     p := p + 1;    1 { | } { | }min f i i n miI n f i p i q     + 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       . Điều này được minh chứng bằng những logic sau:    1 { | } { | }min f i i n min f i p i q     Giả thiết     { | } { | } 1min f i p i q min f i p i q      Vì    f q f p 49 + 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            1 1 { | } { | }min f i i n min f i p i q       . Điều này được minh chứng bằng những logic sau:    1 { | } { | }min f i i n min f i p i q     Giả thiết    f q f p Giả thiết     { | } { | } 1 min f i p i q min f i p i q      Bởi vì với    f q f p thì min( f(p) , f(p+1) ) = min( f(p+1)). 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ã) 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 Với kinh nghiệm có được tôi nhìn nhận rất nhanh vòng lặp thực hiện với một chỉ số lặp i. Giá trị của chỉ số i tăng dần sau mỗi lần thực hiện thân vòng lặp. Vòng lặp kết thúc khi i vượt quá n. Từ đó tôi dự đoán biến t = n – i +1. Bất biến Từ đoạn chương trình trên, tôi có thể khái quát hậu điều kiện là 2 1 n j m j   . Từ kinh nghiệm làm các bài toán tìm bất biến, đối với dạng bài toán này tôi áp dụng kỹ thuật giảm dư hằng, thay biến n bằng biến chỉ số i nhằm mục đích làm cho bất biến phụ thuộc vào biến chỉ số của vòng lặp. Bên cạnh đó tôi nhận thấy bất biến chặn của vòng lặp là 1 1i n   , khi i = n+1 vòng lặp sẽ dừng lại. Từ 50 những dự đoán trê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 Biến chức năng dự đoán của tôi là t = n – i +1. 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      . Giống như bài toán 2, Tôi sẽ chứng minh như sau: i n Theo giả thiết 0n i  Chuyển vế p 1 1n i   Cộng 2 vế với 1 1 0n i   Tính chất của phép so sánh. 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  1i n n i N       1 1n i N    2:m m i    1 1n i N    : 1;i i   1n i N   Khi đó, tôi phải chứng minh vấn đề sau là đúng  1 1 1i n n i N n i N          . Điều đó dễ dàng được kiểm chứng bằng những logic sau: 1n i N   Giả thiết 1 1n i N    Tính chất phép <  1 1n i N    Quy tắc toán học Bất biến b t N  Phép gán, tuần tự Phép gán t N 51 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    b I c I tương đương với việc chứng minh thỏa mãn 1 2 0 1 1 i j i n m j i n                1 1 2 2 0 1 1 1 i j i n m i j                 m := m + i*i 1 1 2 0 1 1 1 i j i n m j                i := i + 1 1 2 0 1 1 i j i n m j              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                      . Thỏa mãn bằng các logic sau: i n Giả thiết 1 1i n   Cộng cả hai vế với 1   1 22 2 0 1 ... 1 i j m j i        Theo giả thiết   1 1 22 2 2 2 2 1 1 2 ... 1 i j m i j i i            Cộng hai vế với 2i . Kết luận: Bất biến và biến tôi dự đoán là đúng. 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 = 0) then m := m + i ∗ i ∗ i; i := i + 1; b I Phép gán, tuần tự Luật phép gán I 52 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: Giống các bài toán 2, 4 ở trên, áp dụng dạng mẫu trong trường hợp có một biến chỉ số vòng lặp i, tôi có biến t = n – i +1. Bất biến: Bài toán trên là bài toán dùng để tính tổng các số chẵn mũ ba không vượt quá n. Tôi có thể đưa ra một hậu điều kiện tổng quát như sau    /2 3 1 2* n j m j   . Với [n/2] nghĩa là n chia cho 2 lấy phần nguyên. Nhận thấy biến chỉ số của vòng lặp là i chạy trong miền giá trị 1 1i n   tạo nên bất biến chặn. Áp dụng kỹ thuật giảm dư hằng tôi thay n bằng biến chỉ số i. Khi đó 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     . Điều này được kiểm chứng bằng những logic sau: i n Theo giả thiết 0n i  Chuyển vế 1 0n i   Tính chất của phép > 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   .  1i n n i N       2 0i mod if then : ;m m i i i    : 1;i i   1n i N   Áp dụng luật điều kiện đối với   2 0 :i mod m m i i i    if then Tôi thấy không thay đổi giá trị của i. khi đó tôi cần chứng minh 1 ( 1) 1i n n i N n i N          . Điều đó được kiểm chứng bằng các logic sau: 1n i N   Theo giả thiết 53 1 1n i N    Định nghĩa của phép < ( 1) 1n i N    Quy tắc toán học Bất biến    1 /2 3 0 1 1 2* i j i n i n m j                      2 0i mod if then : ;m m i i i    : 1;i i     1 /2 3 0 1 1 2* i j i n m j                  Tôi phải chứng minh hai trường hợp sau + Trường hợp 1:    1 /2 3 0 1 1 2* i j i n i n m j                       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                     : ;m m i i i       1 1 /2 3 0 1 1 1 2* i j i n m j                    : 1;i i     1 /2 3 0 1 1 2* i j i n m j                  Tôi cần phải cho thấy b I Luật rẽ nhánh (i mod 2 = 0: true) Luật gán, luật ghép Luật gán {I} 54    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                      . Điều đó được minh chứng bằng những logic sau: 1 1i n   Vì i n 1 1i  Vì 1 i    1 /2 3 0 2* i j m j       Theo giả thiết        1 /2 1 1 /2 3 33 3 0 0 2* 2* i i j j m i j i j                 Vì  1 /2 1 /2i i         với mod2 0i  . + Trường hợp 2:    1 /2 3 0 1 1 2* i j i n i n m j                       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                    : 1;i i     1 /2 3 0 1 1 2* i j i n m j                  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                     . Điều đó được minh chứng bằng những logic sau: b I Luật rẽ nhánh (i mod 2 = 0: false) Luật phép gán {I} 55 1 1i n   Vì i n 1 1i  Vì 1 i    1 /2 3 0 2* i j m j       Theo giả thiết        1 1 /2 1 /2 3 3 0 0 2* 2* i i j j m j j               Vì  1 /2 /2i i        với mod2 0i  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: 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: Giống các bài toán 2, 4, 5 ở trên, áp dụng dạng mẫu trong trường hợp có một biến chỉ số vòng lặp i, tôi có biến t = n – i +1. Bất biến: Bài toán trên là bài toán dùng để tính tổng các số lẻ mũ ba không vượt quá n. Tôi có thể đưa ra một hậu điều kiện tổng quát như sau    1 /2 3 0 2* 1 n j m j       . Với [n/2] nghĩa là n chia cho 2 lấy phần nguyên. Nhận thấy biến chỉ số của vòng lặp 1 1i n   tạo nên bất biến chặn. Áp dụng kỹ thuật giảm dư hằng tôi thay n bằng biến chỉ số i. Khi đó 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 toán 4. Kết luận biến t tìm được thỏa mãn yêu cầu. 56 Bất biến    2 /2 3 0 1 1 2* 1 i j i n i n m j                       2 1i mod if then : ;m m i i i    : 1;i i     1 /2 3 0 1 1 2* 1 i j i n m j                   Tôi phải chứng minh hai trường hợp sau (các phân tích đã được tối giản, có thể xem chi tiết ở bài toán 5). + 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                       . Điều đó được minh chứng bằng những logic sau: 1 1i n   Vì i n 1 1i  Vì 1 i    2 /2 3 0 2* 1 i j m j       Theo giả thiết        2 /2 1 2 /2 3 33 3 0 0 2* 1 2* 1 i i j j m i j i j                   Vì    2 /2 1 1 /2i i          với mod 2 1i  . + Trường hợp 2: Tôi cần phải cho thấy 57    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                      . Điều đó được minh chứng bằng những logic sau: 1 1i n   Vì i n 1 1i  Vì 1 i        1 2 /2 2 /2 3 3 0 0 2* 1 2* 1 i i j j m j j                 Vì    1 2 /2 2 /2i i          với mod2 0i  Kết luận: Bất biến và biến tôi dự đoán là đúng. Bài 7. Cho chương trình (tựa mã) sau: với x,y,z là các biến nguyên, n là một hằng nguyên dương. x = 0 ; y = 1 ; z = 1 ; 1 ≤ n While z < n do begin y := x + y; x := y – x; z := z + 1; end {y = fib n} Tìm biến ( t ) và bất biến ( I ) để chứng minh tính đúng đắn của lệnh chu trình. Giải: Dự đoán biến và bất biến Biến Từ những bài toán đã làm, tôi dễ dàng đưa ra dự đoán biến chức năng của lệnh chu trình trên là t = n – z. Khi z = n vòng lặp sẽ chấm dứt. Bất biến Tôi thấy đoạn chương trình dùng để tính số fibonacci của một số nguyên n (1 ≤ n). Hậu điều kiện tổng quát là y = fib ( n ). Bằng cách thay thế n bởi biến chỉ số trong điều kiện lặp. Với z chạy trong miền giá trị từ 1 đến n, tôi thấy biến x và y lần lượt sẽ nhận các giá trị fib như sau: y = fib (z) và x = fib (z-1). 58 Từ những phân tích và kỹ thuật áp dụng phương pháp giảm dư hằng, tôi đưa ra dự đoán biết biến của vòng lặp là    1I y fib z x fib z z n       Chứng minh biến và bất biến vừa tìm được là đúng. Biến Chứng minh ban đầu t > 0. Tôi phải chứng minh 0b t  . Khi đó, tôi cần chỉ ra rằng 0z n n z    . Điều này hiển nhiên đúng. Chứng minh    b t N c t N   . Áp dụng luật phép gán và phép ghép, tôi có: z n n z N     1n z N   y := x + y; x := y – x;  1n z N   z := z + 1 n z N  Tôi cần chỉ ra rằng  1z n n z N n z N        . Điều đó được minh chứng bằng những logic sau: n z N  Giả thiết 1 1n z N    Trừ 1 cả hai vế  1n z N   1N N  Bất biến Tôi chứng minh    b I c I . Áp dụng luật phép gán và ghép tôi có:    1y fib z x fib z z n z n           1 1 1 1x y fib z x y x fib z z n            y := x + y;    1 1 1 1y fib z y x fib z z n          x := y – x;    1 1 1 1y fib z x fib z z n         z := z + 1    1y fib z x fib z z n      Khi đó, tôi cần phải chỉ ra rằng 59    1y fib z x fib z z n          1 1x y fib z y fib z z n        Điều đó được minh chứng như sau: 1z n  Vì z n  y fib z Theo giả thiết  1x fib z  Theo giả thiết      1 1y x fib z fib z fib z      Tính chất dãy fibonacci Kết luận: Bất biến và biến tôi dự đoán là đúng. Bài 8. Cho chương trình ( tựa mã ) sau: với r, s, x là các biến nguyên, y là một số nguyên dương. r:=0; s:= -1; x:= 0; While r ≤ y do Begin s:= s + 2; r:= r + s; x := x + 1; End Tìm biết ( t ) và bất biến ( I ) để chứng minh tính đúng đắn của lệnh chu trình. Giải: Dự đoán biến và bất biến Biến Nhận thấy biến chỉ số r tăng tuần tự và là bình phương của x. Vòng lặp sẽ kết thúc khi r vượt quá n. Đối với dạng điều kiện lặp có một biến chỉ số (r), theo kinh nghiệm tôi đưa ra một biến chức năng t = n – r + 1. Ở đầu ra của vòng lặp biến chức năng sẽ có giá trị t ≤ 0. Bất biến Phân tích qua đoạn chương trình tôi nhận thấy nó dùng để trả ra phần nguyên căn bậc hai của một số nguyên dương y ([√y] = x -1). Các biến trong thân vòng lặp có giá trị s = 2x - 1, 2r x . Tôi dự đoán một bất biến vòng lặp từ những dữ liệu vừa phân tích   22 2 1 1I r x s x x y        Chứng minh biến và bất biến vừa tìm được là đúng. Biến 60 Xem lại chứng minh ở bài 2, 4, 5, 6. Bất biến Tôi chứng minh    b I c I . Áp dụng vào thân vòng lặp tôi có   22 2 1 1r x s x x y r y         I b   2 22 1 2 2 1r s x s x x y          s:= s + 2;   2 21 2 1r s x s x x y        r:= r + s;   2 21 2 1r x s x x y       x := x + 1;   22 2 1 1r x s x x y       Có   2 22 1 2 2 1r s x s x x y           2 22 1r x s x x y      . Khi đó tôi cần phải chỉ ra   22 2 1 1r x s x x y r y          2 22 1r x s x x y      . Điều đó được minh chứng bằng những logic sau: 2r x Theo giả thiết 2 1s x  Theo giả thiết r y Theo giả thiết 2x y Vì 2r x . Kết luận : Bất biến và biến tôi dự đoán là đúng. Như vậy, 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, hay phương pháp đảm bảo tối ưu. Vì cơ bản những bài toán khác nhau đều 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 các giải pháp được đúc rút ra dựa trên những kinh nghiệm được học hỏi và khám phá trong quá trình tìm tòi. Tất cả các kinh nghiệm đó đã được tôi trình bày trong khi làm các bài toán tìm biến (t) , Bất biến vòng lặp (I), và các bài toán chứng minh tính đúng đắn của chương trình. Luật ghép Luật ghép Luật phép gán I 61 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ự. 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 toán 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 lệnh 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õ 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ụ bài toán 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. Nó góp phần giảm thiểu rủi ro và kinh phí sửa chữa, bảo trì. 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 62 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 chắc sẽ còn 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. 63 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.