Loop invariant là gì?

Bất biến vòng lặp (loop invariant) là điều kiện (condition) về mối quan hệ giữa các biến (variable) trong chương trình của chúng ta mà nó chắc chắn đúng (true) ngay trước và ngay sau mỗi lần lặp (iteration) của vòng lặp (loop).

Ví dụ: hãy xem một vòng lặp for (for loop) đơn giản trông giống như sau:

int j = 9;
for(int i=0; i

Trong ví dụ này, bất biến vòng lặp (loop invariant) là i + j == 9 vì nó đúng với mỗi lần lặp. Một bất biến vòng lặp (loop invariant) khác là i> = 0 && i

Đối với những ai có thể bị nhầm lẫn giữa bất biến vòng lặp (loop invariant) và điều kiện vòng lặp (loop condition) tức là điều kiện kiểm soát sự kết thúc của vòng lặp).

Bất biến vòng lặp (loop invariant) phải true:

• Trước khi vòng lặp bắt đầu
• Trước mỗi lần lặp của vòng lặp
• Sau khi vòng lặp kết thúc (terminate)

Mặc dù nó có thể tạm thời false trong phần thân (body) của vòng lặp). Mặt khác, điều kiện vòng lặp phải là false sau khi vòng lặp kết thúc, nếu không vòng lặp sẽ không bao giờ kết thúc.