Luận văn Một số phương pháp chứng minh tính đúng của thuật toán và ứng dụng

án rồi thì việc phân tích thuật toán vẫn là cần thiết vì sau khi thiết xong cũng không chắc chắn hoàn toàn đó là thuật toán đúng và phù hợp với yêu cầu thực tế. Công việc này cũng có thể phải lặp đi lặp lại nhiều lần. Phân tích thuật toán gồm nhiều vấn đề như phân tích tính đúng, tính hiệu quả, độ phức tạp của thuật toán. 1.3.1. Tính đúng đắn của thuật toán Thiết kế xong một thuật toán câu hỏi luôn luôn phải có đó là thuật toán được thiết kế đã đúng chưa? Cách đơn giản nhất mà được sử dụng thông dụng đó là viết chương trình cho thuật toán đã thiết kế và chạy thử chương trình với nhiều bộ dữ liệu vào cụ thể (tests) để kiểm tra dữ liệu ra có chuẩn xác hay chưa. Tuy nhiên, cách này cũng chỉ khẳng định được thuật toán đúng với các trường hợp cụ thể mà thôi. Có một cách khác chứng minh được thuật toán đúng đó là chứng minh bằng toán học. Nhưng với cách chứng minh thuật toán đúng bằng toán học thì phức tạp hơn nhiều và đòi hỏi nhiều kiến thức tổng hợp cả về toán học và tin học cộng với khả năng của người thực hiện việc chứng minh thuật toán. Chúng ta sẽ nghiên cứu việc này cụ thể hơn ở các chương sau. 1.3.2. Độ phức tạp thuật toán a) Độ phức tạp về mặt thời gian Vấn đề thời gian thực hiện thuật toán cũng là một vấn đề quan trọng vì một thuật toán cho dù có đúng nhưng thời gian thực hiện quá lâu không đáp ứng nhu cầu thực tế thì cũng sẽ không thể hoặc ít được sử dụng. Nên đối với thuật toán người ta luôn quan tâm đến vấn đề sao cho có thể cải tiến để thuật toán nhanh hơn (nhưng chưa chắc ít phức tạp hơn). Để đánh giá về thời gian thực hiện thuật toán ta có thể viết chương trình, chạy thử và đánh giá thời gian thực khi chạy chương trình. Cách này tuy là có thể thực hiện được nhưng lại phụ thuộc vào tốc độ của từng loại máy tính do có thể nhanh trên máy này nhưng lại chậm trên máy khác. Để hạn chế nhược điểm phụ thuộc vào phần cứng máy tính như vậy người nghiên cứu phương pháp đánh giá bằng toán học. Cách này tuy khó thực hiện hơn, phức tạp hơn nhưng đánh giá được ngay cả với dữ liệu có kích thước lớn. Nhưng với đề tài của luận văn ta không nghiên cứu thêm về vấn đề này. b) Độ phức tạp về mặt không gian Không gian ở đây là sự đánh giá về tài nguyên mà chương trình sử dụng, chủ yếu là bộ nhớ máy tính. Do bộ nhớ máy tính là hữu hạn nên nếu dữ liệu đầu vào và các dữ liệu cần lưu trữ trong quá trình xử lý quá lớn vượt quá không gian bộ nhớ, các thiết bị lưu trữ cho phép thì chương trình không thể chạy được. Do vậy khi thiết kế thuật toán hay lựa chọn thuật toán, lựa chọn ngôn ngữ lập trình để viết chương trình ta cũng phải qua tâm đến những vấn đề này để đạt hiệu quả mong muốn. CHƯƠNG 2. MỘT SỐ PHƯƠNG PHÁP CHỨNG MINH TÍNH ĐÚNG CỦA THUẬT TOÁN Chúng ta đã biết thuật toán là vô cùng quan trọng và có thể nói là thuật toán mang tính chất quyết định để giải một bài toán trên máy tính. Nhưng một thuật toán vừa thiết kế xong chưa thể khẳng định được ngay là thuật toán đó có đúng hay không. Ở chương này nghiên cứu tổng quan về các chiến lược chứng minh tính đúng của thuật toán. Nghiên cứu chi tiết về chiến lược chứng minh tính đúng của thuật toán một cách trực tiếp dựa vào toán học mà không cần chạy các bộ test chương trình cụ thể. 2.1. Các chiến lược chứng minh tính đúng thuật toán Để kiểm tra thuật toán có đúng hay không ta có nhiều chiến lược như kiểm thử, chứng minh tính đúng hoặc kết hợp cả kiểm thử và chứng minh tính đúng nhưng mỗi chiến lược đều có ưu, nhược điểm riêng. Sau đây là một số đặc điểm sơ lược về mỗi chiến lược. Kiểm thử (Testing): Để kiểm tra tính đúng đắn của thuật toán chúng ta có thể cài đặt thuật toán đó và cho thực hiện trên máy với một số bộ dữ liệu mẫu rồi lấy kết quả thu được so sánh với kết quả đã biết. Có thể phải có rất nhiều bộ dữ liệu vào với kích cỡ khác nhau mới kiểm tra được hết các trường hợp của bài toán đặt ra nhưng cũng có khả năng người lập trình không phát hiện ra hết các trường hợp. Thực ra thì cách làm này không chắc chắn bởi vì có thể thuật toán đúng với tất cả các bộ dữ liệu chúng ta đã thử nhưng lại sai với một bộ dữ liệu nào đó. Do đó với chiến lược này là tương đối dễ thực hiện nhưng lại không thể phát hiện hết các lỗi tiểm ẩn. Vả lại cách làm này chỉ phát hiện ra thuật toán sai chứ chưa chứng minh được là nó đúng. Tính đúng đắn của thuật toán cần phải được chứng minh bằng toán học. Tuy nhiên kiểm thử vẫn được sử dụng phổ biến cho các chương trình trong thực tế, vì các chương trình lớn khó có thể chứng minh hoàn toàn bằng toán học. Hiện nay, trong công nghệ phần mềm công đoạn kiểm thử là bắt buộc. Chứng minh tính đúng (Correctness proof): Với chiến lược chứng minh tính đúng của thuật toán cần dùng các kiến thức toán học để chứng minh thuật toán đúng. Cách này chứng minh được cho bài toán tổng quát nhưng đòi hỏi tư duy trừu tượng và logic toán học chặt chẽ. Có các phương pháp chứng minh tính đúng của thuật toán như phương pháp quy nạp, phương pháp bất biến vòng lặp. Đây cũng là nội dung nghiên cứu chủ yếu khi thực hiện luận văn này. Kết hợp kiểm thử và chứng minh tính đúng: Để đảm bảo tính đúng của thuật toán một cách chặt chẽ hơn nữa ta có thể kết hợp cả hai chiến lược kiểm thử và chứng minh tính đúng đã nêu ở trên. 2.2. Các phương pháp chứng minh tính đúng (Correctness proofs) Làm thế nào để biết thuật toán hoạt động thế nào? Cách tốt nhất là chứng minh thuật toán là đúng. Có một số phương pháp chứng minh tính đúng của thuật toán như: Đối với các thuật toán đệ quy có thể chứng minh tính đúng bằng phương pháp quy nạp. Đối với các thuật toán không đệ quy có thể sử dụng phương pháp bất biến vòng lặp cho mọi vòng lặp. 2.2.1. Phương pháp quy nạp (induction) a) Phương pháp quy nạp toán học Gọi P(n) là một phát biểu nào đó liên quan đến biến số tự nhiên n (n ≥ n0). Chứng minh bằng quy nạp sẽ gồm các bước sau: Bước 1: gọi là bước khởi điểm. Chúng ta sẽ chứng minh P(n) đúng cho trường hợp đầu tiên n = n0 . Bước 2: gọi là bước quy nạp. Đây là bước quan trọng nhất. Ở bước này, giả sử rằng P(n) đúng cho các trường hợp n0 ≤ n ≤ k, chúng ta cần chứng minh P(n) cũng đúng với trường hợp n = k+1. Từ hai bước này, theo nguyên lý quy nạp toán học, chúng ta sẽ kết luận rằng P(n) sẽ đúng với mọi số tự nhiên n ≥ n0. Cách sử dụng phương pháp quy nạp toán học để chứng minh tính đúng của thuật toán sẽ được trình bày cụ thể sau đây. b) Chứng minh tính đúng của thuật toán bằng phương pháp quy nạp Các thuật toán nếu chỉ có các dòng lệnh đơn lẻ không có chứa đệ quy hay lặp thì ta dễ dàng thấy được tính đúng của nó nhưng với các thuật toán có chứa đệ quy hay vòng lặp thì việc chứng minh trở nên phức tạp hơn. Sau đây ta sử dụng phương pháp quy nạp toán học đã nêu ở trên để chứng minh tính đúng của thuật toán đệ quy. Ta sẽ chứng minh tính đúng của thuật toán đệ quy bằng phương pháp quy nạp theo kích thước dữ liệu vào như sau: Cơ sở của quy nạp: Trường hợp suy biến của đệ quy. Đây cũng chính là điều kiện phải có để thuật toán có tính dừng. Giả thiết quy nạp: Giả sử thuật toán đúng với dữ liệu kích thước n. Tổng quát: Chứng minh thuật toán đúng với dữ liệu kích thước n+1. c) Một số ví dụ Bài toán 2.1. Tính giai thừa. Tính giai thừa của một số nguyên dương n cho trước. Input: Số nguyên dương n. Output: n! Thuật toán: Giaithua(n): int; //Hàm đệ quy tính n! if (n = 0) or (n = 1) then return 1 else return (n * Giaithua(n - 1)); End. Chứng minh: Chứng minh tính đúng của thuật toán theo phương pháp quy nạp như sau: Cơ sở quy nạp: Với n = 0 hoặc n = 1 thì Giaithua(0) = Giaithua(1) = 1. Tức là: 0! = 1! = 1. Như vậy thuật toán luôn đúng trong trường hợp cơ sở. Giả thiết quy nạp: Giả sử thuật toán đúng với n. Tức là ta có: Giaithua(n) = n! Tổng quát: ta chứng minh thuật toán đúng đắn với n+ 1, tức là phải chứng minh Giathua(n + 1) = (n + 1)!. Thật vậy: Ta có: Giaithua(n + 1) = (n + 1)*Giaithua(n) = (n + 1)*n! //Theo giả thiết quy nạp = (n + 1)! Vậy thuật toán tính giai thừa của số nguyên dương n là thuật toán đúng. Bài toán 2.2. Tìm max. Tìm giá trị lớn nhất của một dãy số có n phần tử A1, A2,, An. Input: Số nguyên dương n và dãy số A1, A2,, An. Output: max. Thuật toán đệ quy: Maximum(n); //Trả về giá trị max của dãy số có n phần tử if (n=1) then Maximum=A1 else Maximum=(max(Maximum(n-1), An); End. Chứng minh: Thuật toán trả lại đúng giá trị lớn nhất trong các phần tử A1, A2, , An. Thậy vậy: Cơ sở quy nạp: n=1 nên A1 là phần tử duy nhất và lớn nhất. Giả thiết quy nạp: Maximum(n) trả lại giá trị max(A1, A2, , An). Tổng quát: Maximum(n+1) trả lại max(Maximum(n), An+1) = max(A1, A2, , An, An+1). Như vậy theo phương pháp chứng minh quy nạp thuật toán đệ quy tìm giá trị max là thuật toán đúng. Bài toán 2.3. Tháp Hà Nội. Phát biểu bài toán: Khởi đầu có 3 cọc, trong đó có 2 cọc rỗng và một cọc chứa một số lượng nhất định các đĩa kích thước khác nhau xếp theo thứ tự bé ở trên, lớn ở dưới. Trò chơi kết thúc khi toàn bộ đĩa từ một cọc ban đầu được chuyển sang một cọc khác theo đúng thứ tự bé ở trên, lớn ở dưới. Với yếu cầu khi chuyển như sau: Mỗi lần chỉ được di chuyển một đĩa từ cọc này sang cọc khác. Khi di chuyển phải di chuyển đĩa ở trên cùng. Khi đặt đĩa vào cọc nào đó cũng phải đặt ở trên cùng. Không được phép đặt đĩa to hơn lên trên đĩa bé hơn. Thuật toán: ChuyenThap(n, A, B, C) º; //Chuyển n tầng từ A→B; C trung gian. if (n=1) then Chuyen1Tang(A, B); else ChuyenThap(n-1, A, C, B); Chuyen1Tang(A, B); ChuyenThap(n-1, C, B, A); endelse; End. Chứng minh: Cơ sở quy nạp: Chuyển một tầng tháp từ cọc A sang cọc B lấy cọc C làm trung gian ChuyenThap(1, A, B, C) = Chuyen1Tang(A, B). Giả thiết quy nạp: Giả sử thuật toán đúng khi chuyển n tầng tháp từ cọc A sang cọc B lấy cọc C làm trung gian ChuyenThap(n, A, B, C). Tức là ngay sau khi thủ tục này được thực hiện ta có n tầng tháp được sắp đúng thứ tự nhỏ ỏ trên, lớn ở dưới trên cọc B. Tổng quát: Ta chứng minh thuật toán vẫn đúng khi chuyển n+1 tầng từ cọc A sang cọc B lấy cọc C làm trung gian. Thật vậy ChuyenThap(n+1, A, B, C) cần thực hiện các công việc sau: ChuyenThap(n, A, C, B); {Chuyển n tầng từ cọc A sang cọc C lấy cọc B làm trung gian.} Chuyen1Tang(A, B); {Chuyển 1 tầng từ cọc A sang cọc B nên B có 1 tầng đồng thời là tầng lớn nhất.} ChuyenThap(n, C, B, A); {Chuyển n tầng từ cọc C sang cọc B. Vì vậy B có thêm n tầng nữa theo giả thiết quy nạp thì n tầng này đã được sắp đúng thứ tự.} Như vậy B có n+1 tầng được sắp đúng thứ tự sau khi thực hiện thủ tục đệ quy ChuyenThap(n+1, A, B, C). Do đó thuật toán chuyển tháp đệ quy là thuật toán đúng. Bài toán 2.4. Nhân 2 số tự nhiên. Thuật toán: Multi(a, b); //Hàm trả lại tích số ab if b=0 then multi=0 else if (b is odd) then multi = multi(2a, [b/2]) + a) else multi = multi(2a, [b/2]); End. Chứng minh: Không mất tổng quát ta sử dụng phương pháp quy nạp trên b để chứng minh tính đúng của thuật toán. Hàm multi(a, b) trả lại giá trị tích ab. Giả thiết thuật toán đúng với b=0, thật vậy multi(a, 0) trả lại giá trị là 0. Giả sử rằng với mọi số tự nhiên b³0, hàm multi(a, b) trả lại giá trị tích ab. Ta phải chứng minh rằng multi(a, b+1) trả lại giá trị tích a(b+1). Xảy ra hai trường hợp dựa vào giá trị b+1 lẻ hoặc b chẵn. Ta có: Nếu b+1 lẻ thì multi(a, b+1) trả lại giá trị: multi(2a, [(b+1)/2]) + a = = 2a([(b+1)/2]) + a = 2a(b/2) + a = ab + a = a(b+1). Nếu b+1 chẵn thì multi(a, b+1) trả lại giá trị: multi(2a, [(b+1)/2]) = = 2a(b+1)/2 = a(b+1). Như vậy cả hai trường hợp ta đều có multi(a, b+1) trả lại giá trị là tích a(b+1). Do đó thuật toán trên là đúng đắn. Bài toán 2.5. Tính số Fibonacci thứ n. Dãy số Fibonacci bắt nguồn từ bài toán cổ về việc sinh sản của các cặp thỏ. Bài toán đặt ra như sau: 1) Các con thỏ không bao giờ chết. 2) Hai tháng sau khi ra đời, mỗi cặp thỏ mới sẽ sinh ra một cặp thỏ con gồm một đực, một cái. 3) Khi đã sinh con rồi thì cứ mỗi tháng tiếp theo chúng lại sinh được một cặp con mới. Giả sử từ đầu tháng 1 có một cặp mới ra đời thì đến giữa tháng thứ n sẽ có bao nhiêu cặp? Ví dụ, n = 6, ta thấy: Tháng thứ 1: 1 cặp (AB) (Cặp ban đầu) Tháng thứ 2: 1 cặp (AB) (Cặp ban đầu vẫn chưa đẻ) Tháng thứ 3: 2 cặp (AB)(CD) (Cặp ban đầu đẻ ra thêm 1 cặp con CD) Tháng thứ 4: 3 cặp (AB)(CD)(EF) (Cặp ban đầu tiếp tục đẻ, cặp CD chưa đẻ) Tháng thứ 5: 5 cặp (AB)(CD)(EF)(GH)(IK) (Cả 2 cặp (AB) và (CD) cùng đẻ, cặp (EF) chưa đẻ). Tháng thứ 6: 8 cặp (AB)(CD)(EF)(GH)(IK) (cả 3 cặp (AB), (CD) và (EF) cùng đẻ). Sau đây ta xét tới việc tính số cặp thỏ ở tháng thứ n, kí hiệu Fn: Nếu mỗi cặp thỏ ở tháng thứ n-1 đều sinh ra một cặp thỏ con thì số cặp thỏ ở tháng thứ n sẽ là: Fn=2*Fn - 1. Nhưng vấn đề không phải như vậy, trong các cặp thỏ ở tháng thứ n - 1, chỉ có những cặp thỏ đã có ở tháng thứ n-2 mới sinh con ở tháng thứ n được thôi. Do đó Fn=Fn - 1+Fn - 2 (=số cũ + số sinh ra). Vậy có thể tính được Fn theo công thức sau: Fn=1 nếu n=1 hoặc n=2 Fn=Fn - 1+Fn - 2 nếu n³3 Như vậy ta có bài toán: Tính số Fibonacci thứ n, kí hiệu Fn. Biết: F1=1; F2=1; Fn=Fn-1+Fn-2 với n³3 Input: Số nguyên dương n. Output: Số Fibonacci thứ n, tức là Fn. Thuật toán: Fib(n); //Hàm đệ quy tính số Fibonacci thứ n if (n = 1) or (n = 2) then Fib = 1 else Fib = Fib(n - 1) + Fib(n - 2); End. Chứng minh: Cơ sở quy nạp: Nếu n = 1 hoặc n = 2 thì Fib =1. Giả thiết quy nạp: Giả sử thuật toán đúng với n tức là ta có: Fib(n) = Fib(n-1) + Fib(n-2) Tổng quát: Ta phải chứng minh thuật toán đúng với n+1. Tức là phải chứng minh: Fib(n+1) = Fib(n) + Fib(n-1). Thật vậy: Fib(n+1) = Fib((n+1)-1) + Fib((n+1)-2) = Fib(n) + Fib(n-1). Như vậy thuật toán tính số Fibonacci thứ n là thuật toán đúng. 2.2.2. Phương pháp bất biến vòng lặp (loop invariant) Các thuật toán không đệ quy gồm có các thành phần: các câu lệnh, biểu thức, vòng lặp. Do ta khó có thể xác định hết các trường hợp khi vòng lặp được thực hiện trong khi các thành phần còn lại của thuật toán ta có thể dễ dàng kiểm tra được tính đúng đắn của chúng. Vì thế, tính chính xác của các thuật toán này chủ yếu phụ thuộc vào các vòng lặp. Do vậy, để chứng minh thuật toán là đúng ta có thể chứng minh vòng lặp được thực hiện đúng bằng bất biến trong vòng lặp. a) Chứng minh tính đúng của thuật toán bằng phương pháp bất biến vòng lặp Chứng minh tính đúng của thuật toán lặp bằng phương phương pháp bất biến vòng lặp có các đặc điểm như sau: Bất biến vòng lặp là biểu thức logic (của các biến được sử dụng vòng lặp) có giá trị không đổi trong quá trình lặp. Tại mỗi thời điểm của thuật toán chỉ có một vòng lặp, nếu có vòng lặp lồng nhau thì phải bắt đầu từ các vòng lặp bên trong. Sau mỗi vòng lặp bất biến vòng lặp sẽ trả lại kết quả đúng và sự đúng này phải được duy trì ở các vòng lặp tiếp theo.Sử dụng bất biến vòng lặp để chỉ ra thuật toán lặp là có tính dừng. Thông qua sự kết thúc các điều kiện chứng minh rằng thuật toán cho kết quả đúng. Như đã nói ở trên, bất biến vòng lặp là một biểu thức logic có giá trị không đổi trước mỗi vòng lặp. Từ bất biến vòng lặp, ta có thể chứng minh tính đúng của những thuật toán có chứa các vòng lặp. Tuy nhiên, không phải cứ một biểu thức nào không đổi ta cũng cho nó là bất biến vòng lặp. Sau đây ta xét một ví dụ để làm rõ hơn nhận định này. Ví dụ: Bài toán nối chuỗi. Bài toán: Có hai chuỗi S1 và S2. Yêu cầu nối S2 vào cuối S1. Input: S1, S2. Output: S1= S1*S2. Thuật toán: Noi_chuoi(S1, S2) while (length(S2)>0) do x=S2[1]; //lấy ra phần tử đầu chuỗi S2 S1=S1+x; //thêm phần tử vừa lấy ra vào cuối S1 Delete(S2(1,1)); endwhile. Những mệnh đề không đổi trước mỗi vòng lặp: Độ dài của các chuỗi trước mỗi vòng lặp đều không âm: |S1|³0, |S2|³0. Điều này đúng, vì độ dài của bất kì một chuỗi nào cũng không âm. Điều này là hiển nhiên. Bởi vậy, nó chẳng đem lại hữu ích gì cho chúng ta trong việc chứng minh tính đúng của thuật toán. Tổng độ dài của hai chuỗi S1 và S2 không đổi: |S1|+|S2| = const. Điều này đúng. Vì trong thuật toán ta chỉ chuyển các kí tự từ chuỗi này sang chuỗi khác thôi chứ không tạo thêm mới kí tự nào. Tuy nhiên, dựa vào nhận định này ta cũng chưa thể khẳng định rằng khi kết thúc vòng lặp thì chuỗi S2 được nối vào S1. S1*S2 là không đổi trước mỗi vòng lặp. Nhận định này đúng, và hữu ích hơn nhận định trước. Bởi vì nếu S1*S2 là không đổi thì |S1|+|S2| cũng không đổi. Khi kết thúc vòng lặp, tức là |S2|=0. Lúc này: S1*S2=S1= #S1 *#S2 do S1*S2 luôn không đổi (kí hiệu # chỉ đến giá trị đầu vào của S1 và S2). Vậy khi vòng lặp kết thúc ta được chuỗi S1 mà đã nối S2 vào cuối. Nhận định: S1*S2 là không đổi trước mỗi vòng lặp cho ta tính chất hữu ích giúp ta chứng minh được thuật toán đúng. Do đó, nó chính là bất biến vòng lặp cần tìm. Từ ví dụ trên ta nhận thấy, trong một vòng lặp có thể có rất nhiều những biểu thức không đổi trong quá trình lặp, nhưng không phải biểu thức nào cũng cho ta những tính chất hữu ích để chứng minh được tính đúng của thuật toán. Vậy làm thế nào để xác định được đâu là một bất biến vòng lặp giúp ta chứng minh tính đúng của thuật toán? Sau đây là các đặc trưng của bất biến vòng lặp để phân biệt nó với những biểu thức không đổi khác trong vòng lặp. b) Các đặc trưng của bất biến vòng lặp Khởi tạo: bất biến của vòng lặp phải đúng trước lần lặp đầu tiên. Duy trì: Nếu bất biến vòng lặp đúng trước một vòng lặp thì bất biến vòng lặp vẫn còn đúng trước vòng lặp tiếp theo. Kết thúc: Khi vòng lặp kết thúc, bất biến vòng lặp này cho chúng ta một tính chất hữu ích giúp chứng minh được thuật toán là đúng đắn. c) Một số ví dụ Bài toán 2.6: Tìm min. Tìm giá trị nhỏ nhất (min) của một dãy số gồm n phần tử A1, A2,, An. Input: Số nguyên dương n và dãy số A1, A2,, An. Output: min. Thuật toán không đệ quy: Minimum(n,A)º; //Tìm min của dãy số có n phần tử m=A1; for i=2 to n do if (m>Ai) then m=Ai; Minimum = m; End. Chứng minh: Xác định bất biến vòng lặp: Theo thuật toán ta xét dần các phần tử từ A1, A2, , An. Ở bước thứ j ta có giá trị nhỏ nhất kí hiệu là mj chính là giá trị nhỏ nhất trong dãy các số A1, A2, , Aj, như vậy mj = min(A1, A2, , Aj). Khởi tạo: Dãy số đang xét chỉ có một phần tử duy nhất là A1 nên ta có m1= m=A1=min(A1). Vì vậy bất biến vòng lặp đúng trước vòng lặp đầu tiên. Duy trì: Giả sử bất biến vòng lặp đúng sau bước thứ j và ta có mj = min(A1, A2, , Aj) ta chứng minh bất biến vòng lặp vẫn đúng sau bước tiếp theo, thật vậy: mj+1 = min(mj, Aj+1) = min(A1, A2, , Aj+1). Như vậy mj+1 là giá trị nhỏ nhất của dãy số từ A1, A2, , Aj+1 hay bất biến vòng lặp là đúng. Kết thúc: Khi i=n+1 sau t lần lặp (t=n+1-1=n) thì mt= min(A1, A2, , At) = min(A1, A2, , An). Như sau khi kết thúc thuật toán trả về giá trị nhỏ nhất của dãy số đã cho. Vậy thuật toán tìm giá trị nhỏ nhất ở trên là thuật toán đúng. Bài toán 2.7. Sắp xếp. Sắp xếp một dãy n các số cho trước a1, a2, , an thành dãy không giảm. Input: Số n và dãy gồm n số . Output: Một hoán vị của chuỗi đầu vào thỏa mãn: a'1 £ a'2 £ £ a'n. Thuật toán sắp xếp chèn (Insertion Sort): Tư tưởng của thuật toán sắp xếp chèn là tăng dần bằng cách thêm một phần tử a[j] vào đúng vị trí trong mảng đã được sắp xếp thứ tự a[1..j-1] sao cho đảm bảo trật tự cho mảng a[1..j] cũng là mảng được sắp. Đó cũng chính là bất biến vòng lặp cần xét. Sap_xep(n,a)º; for j=2 to n do //n là số phần tử của dãy số đã cho key=a[j]; //Chèn a[j] vào dãy đã được sắp a[1..j-1] i=j-1; while (i>0) and (a[i]>key) do a[i+1]=a[i]; i=i-1; endwhile; a[i+1]=key; //chèn phần tử key vào đúng vị trí endfor; End. Chứng minh: Xác định bất biến vòng lặp là mảng con đã được sắp thứ tự a[1..j-1]. Khởi tạo: Khi j=2 thì dãy con a[1..j-1] chứa một phần tử duy nhất là a[1]. Như vậy mảng này cũng là được sắp vì có duy nhất một phần tử. Vì vậy bất biến vòng lặp đúng trước vòng lặp đầu tiên. Duy trì: Tiếp theo, ta kiểm tra tính đúng có được duy trì sau mỗi vòng lặp. Với mỗi j của vòng lặp for thì các phần tử a[j-1], a[j-2],... sang phải một vị trí cho đến khi vị trí thích hợp cho a[j] được tìm thấy. Tại thời điểm đó a[j] được chèn vào đúng vị trí. Như vậy sau một vòng lặp j chuyển sang giá trị tiếp theo thì bất biến vòng lặp được duy trì tức là a[1..j-1] đã được sắp thứ tự. Kết thúc: Cuối cùng, xét khi vòng lặp kết thúc tức là j vượt quá n hay j=n+1. Thay n+1 cho j ta nhận được mảng a[1..n+1-1]=a[1..n] đã được sắp thứ tự. Như vậy toàn bộ dãy số đã được sắp thứ tự khi vòng lặp kết thúc. Do đó thuật toán sắp xếp chèn là thuật toán đúng. Mặc dù thuật toán sắp xếp chèn (chèn trực tiếp) có vẻ nhanh và thực tế là thuật toán này nhanh với n đủ nhỏ. Khi n càng lớn thì thuật toán sắp xếp chèn trở nên càng chậm vì độ phức tạp về mặt thời gian của thuật toán này là O(n2). Do khi n càng lớn thì n2 càng tăng nhanh hơn. Sau đây chúng ta nghiên cứu một thuật toán sắp xếp có độ phức tạp thời gian là O(nlgn). Sự ưu việt về mặt thời gian của thuật toán này càng thể hiện rõ khi n càng lớn (cỡ khoảng n³30). Thuật toán sắp xếp trộn (Merge Sort): Tư tưởng của thuật toán sắp xếp trộn đó là chia để trị như phương pháp chia để trị đã trình bày ở chương 1. Cách làm như sau: chia dãy số cần sắp xếp gồm n phần tử thành hai phần mỗi phần gồm n/2 phần tử. Sau đó sắp xếp không giảm hai dãy con đó một cách đệ quy sử dụng sắp xếp trộn. Sau đó kết hợp hai dãy con đã sắp xếp để tạo ra kết quả. Bước cuối cùng trộn hai dãy số con gồm n/2 phần tử đã sắp xếp để được dãy số n phần tử được sắp thành dãy số không giảm. Đệ quy dừng khi dãy cần sắp có độ dài bằng một, trong trường hợp này hiển nhiên ta cũng không cần phải sắp xếp gì cả. Thuật toán sắp xếp trộn có thao tác chính là việc trộn hai dãy con đã được sắp để được dãy mới sắp thứ tự có số phần tử gấp đôi. Để trộn hai dãy con vào với nhau ta sử dụng thủ tục trộn Merge(a, p,q,t) trong đó a là một mảng và p, q, t là các chỉ số của mảng. Giả thiết là các mảng con a[p..q] và a[q+1..t] đã được sắp xếp và ta cần trộn hai mảng con này để được mảng a[p..t] đã được sắp thứ tự. Để cho thuật toán được đơn giản hơn ta sử dụng hai lính canh để biểu thị mảng là rỗng (theo nghĩa là đã lấy hết các phần tử cần sắp của dãy số ban đầu) với giá trị lính canh là vô cùng lớn +¥. Thủ tục trộn như sau: Merge(a, p, q, t)º; n1=q–p+1; n2=t–q ; for i=1 to n1 do l[i]=a[p+i-1]; //Tạo mảng l[1..n1] for j=1 to n2 do R[j]=a[q+j]; //Tạo mảng r[1..n2] l[n1+1]=+¥; //Phần tử lính canh r[n2+1]=+¥; //Phần tử lính canh i=1; j=1; for k=p to t do if l[i]£r[j] then a[k]=l[i]; // Lấy phần tử nhỏ nhất ở mảng l i=i+1 //Chuyển sang phần tử tiếp theo của mảng l else a[k]=r[j]; // Lấy phần tử nhỏ nhất ở dãy mảng r j=j+1; //Chuyển sang phần tử tiếp theo của mảng r endelse; End. Chứng minh: Ta sẽ chứng minh thủ tục trộn trên đây là đúng đắn. Xác định bất biến vòng lặp: Tại mỗi thời điểm bắt đầu của vòng lặp for (dòng thứ 9) để tạo ra mảng a được sắp thì mảng con a[p..k-1] chứa k-p phần tử nhỏ nhất của hai mảng l[1..n1+1] và r[1..n2+1] theo thứ tự đã được sắp là không giảm. Đồng thời l[i] và r[j] là các phần tử nhỏ nhất của các mảng tương ứng l, r mà chưa được chép vào mảng a. Ta chứng minh bất biến vòng lặp đúng trước vòng lặp đầu tiên for (dòng thứ 9) để tạo mảng kết quả a, thật vậy: Khởi tạo: Trước lần lặp đầu tiên k=p nên mảng con a[p..k-1] chứa k-p=0 phần tử nhỏ nhất của l, r hay nói cách khác mảng a rỗng. Đồng thời i=j=1 nên cả l[i] và r[j] đều là các phần tử nhỏ nhất của hai mảng tương ứng l, r do hai mảng này đã được sắp thứ tự không giảm. Tiếp tục ta chứng minh bất biến này được duy trì sau mỗi lần lặp: Duy trì: Không mất tổng quát, giả sử l[i]≤r[j] thì l[i] là phần tử nhỏ nhất tiếp theo được sao chép vào mảng a. Do mảng con a[p..k-1] đã chứa k-p phần tử nhỏ nhất được sắp thứ tự không giảm, sau khi thêm vào phần tử a[k]≥a[k-1] (vì tất cả các phần tử cho vào mảng a trước đều nhỏ hơn a[k]) vào mảng a ta được mảng con a[p..k] cũng là mảng được sắp đúng thứ tự. Đồng thời chỉ số i tăng lên một để chuyển sang phần tử nhỏ nhất trong dãy còn lại của mảng l. Ngược lại, ta làm thao tác tương tự như đối với mảng r sau đó tăng j lên một để chuyển sang phần tử nhỏ nhất trong dãy còn lại của mảng r. Như bất biến vòng lặp được duy trì đúng sau mỗi vòng lặp. Kết thúc: vòng lặp kết thúc khi k = t+1. Khi đó do tính chất của bất biến vòng lặp ta có mảng con a[p..k-1] chính là mảng a[p..t] chứa k-p = t+1-p = t-p+1 phần tử của hai mảng l[1..n1+1] và r[1..n2+1] theo thứ tự được sắp không giảm. Tổng hai mảng l, r có n1+1+n2+1 = q-p+2+t-q+1 = t-p+3 phần tử. Như vậy, trong mỗi mảng l và r chỉ còn lại một phần tử lính canh có giá trị vô cùng lớn +∞. Hay nói cách khác thì tất cả các phần tử không phải là lính canh đã được chép vào mảng a theo thứ tự được sắp không giảm đầy đủ t-p+1 phần tử. Như vậy thuật toán thủ tục sắp xếp trộn là đúng đắn. Bài toán 2.8: Tìm ước chung lớn nhất. Tìm ước chung lớn nhất của hai số nguyên dương a,b. Thuật toán Euclid: ucln(a,b) º; m=a; n=b; r=a mod b; while (r > 0) do m=n; n=r ; r=m mod n endwhile; return n; end. Để chứng minh tính đúng của thuật toán Euclid, ta cần chỉ ra rằng sau mỗi lần lặp khẳng định sau đây được giữ nguyên: m>0, n>0; ucln(m,n) = ucln(a,b). Chứng