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á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í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,. | Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C 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 là một sự tổng quát hóa của mục tiêu post là một trườ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ông rỗ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 minh họ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ảng tươ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ủa mảng một phần tử chính là phần tử đó. 73 Tì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 trong POST phát sinh ra một điểm tiến đến gần POST hơn nhưng vẫn thuộc INV. Trong ví 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ằng phầ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. Đây là 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ày thì đượ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 ta chấ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ải nhấ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 đi lặp lại nhất định. . 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 .
