TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 7

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#Hình 13-1: Một vòng lặp tính toánMột tính toán bằng vòng lặp gồm những thành phần sau: Mục tiêu post, là một hậu điều kiện, được định nghĩa như là một thuộc tính mà bất cứ trạng thái cuối nào của sự tính toán đều phải thỏa mản. Ví dụ như: “Result là giá trị lớn nhất của mảng”. Mục tiêu này được biểu diễn trong hình minh họa là một tập hợp những trạng thái POST thỏa mãn post. Điều kiện bất biến inv,...
Nội dung trích xuất từ tài liệu:
TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 7Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Hình 13-1: Một vòng lặp tính toán Một tính toán bằng vòng lặp gồm những thành phần sau: Mục tiêu post, là một hậu điều kiện, được định nghĩa như là một thuộc tínhmà bất cứ trạng thái cuối nào của sự tính toán đều phải thỏa mản. Ví dụ như:“Result là giá trị lớn nhất của mảng”. Mục tiêu này được biểu diễn trong hình minhhọa là một tập hợp những trạng thái POST thỏa mãn post. Điều kiện bất biến inv, là một sự tổng quát hóa của mục tiêu (post là mộttrường hợp đặc biệt của inv). Ví dụ: “Result là giá trị lớn nhất của phần mảng khôngrỗng bắt đầu từ biên thấp nhất”. Điều kiện bất biến được biểu diễn trong hình minhhọa là một tập hợp những trạng thái INV thỏa mãn inv. Điểm khởi động init thuộc INV, điểm này thỏa mãn điều kiện bất biến. Vídụ: khi giá trị của i là biên dưới của mảng và giá trị của Result là phần tử mảngtương ứng tại vị trí đó, thỏa mãn điều kiện bất biến bởi vì phần tử lớn nhất củamảng một phần tử chính là phần tử đó. 73Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Sự biến đổi body (bắt đầu từ một điểm trong INV chứ không phải trongPOST) phát sinh ra một điểm tiến đến gần POST hơn nhưng vẫn thuộc INV. Trongví dụ trên, sự biến đổi này mở rộng mảng lên từng phần tử và thay thế Result bằngphần tử thêm đó nếu nó lớn hơn Result. Thân vòng lặp trong hàm maxarray ví dụ ởtrên là cài đặt của sự biến đổi này. Biên trên dựa vào số body cần thiết để đưa điểm trong INV đến POST. Đâylà biến. Tính toán xấp xỉ là phương pháp chính của toán giải tích, nhưng ý tưởng nàythì được áp dụng rộng rãi hơn. Sự khác biệt cơ bản là trong toán học thuần túy, tachấp nhận có sự tồn tại của một giới hạn, mặc dù không thể đạt được giới hạn đó.Ví dụ như 1/n có giới hạn là 0 nhưng không có n cụ thể nào để đạt được giới hạnđó. Còn trong tin học, chúng ta cần có được kết quả cụ thể, cho nên chúng ta phảinhấn mạnh rằng tất cả các sự xấp xỉ đều tiến đến kết quả cụ thể sau một số lần lặp đilặp lại nhất định. 13.4. Cú pháp của vòng lặp − Gồm những thành phần sau: Điều kiện bất biến (invariant) của vòng lặp inv – đây là một xác nhận − Điều kiện thoát khỏi vòng lặp exit. − Điều kiện biến đổi (variant) của vòng lặp var – đây là một biểu thức − nguyên. Tập lệnh khởi tạo init, tập lệnh này luôn tạo ra một trạng thái thỏa inv − và làm var không âm. − Tập lệnh body, tập lệnh này, khi khởi đầu một trạng thái mà inv được giữ và var không âm, sẽ bảo vệ điều kiện bất biến và làm điều kiện biến đổi giảm đi (nhưng vẫn bảo đảm không âm). Vì vậy, trong trạng thái kết quả, inv được thỏa và var có giá trị nhỏ hơn trước (nhưng luôn không âm). Tóm lại, vòng lặp có cú pháp như sau: 74Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# from init invariant inv variant var until exit loop body end Đây là phiên bản vòng lặp cho hàm maxarray: from i := t.lower; Result := t @ lower invariant -- Result là giá trị lớn nhất của t khi chỉ số t.lower = i. variant t.lower – i until i = t.upper loop i := i + 1 Result := Result.max (t @ i) end Dưới đây là một ví dụ khác về điều kiện bất biến, đây là hàm tính ước chunglớn nhất (greatest common divisor - gcd) của 2 số nguyên dương a, b bằng thuậttoán Euclid. Phiên bản không có không có điều kiện bất biến và điều kiện biến đổi: 75Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# gcd (a, b: INTEGER): INTEGER is -- Uớc chung lớn nhất của a và b require a > 0; b > 0 local x, y: INTEGER do from x := a; y := b until x=y loop if x>y then x:=x–y else y:=y–x end end Result := x ensure -- Result là ước chung lớn nhất của a và b end Làm sao chắc chắn được rằng hàm gcd trả về đúng giá trị ước chung lớn nhấtcủa a và b. Có một cách để kiểm tra điều này, lưu ý rằng thuộc tính này luôn đúngtrong suốt ...