Loop Invariant
লুপ অপরিবর্তক
একটা predicate যা loop-এর প্রতিটা iteration-এর শেষে সত্য থাকে। Initialization, maintenance আর termination — এই তিন ধাপে প্রমাণ করলে loop-এর correctness প্রমাণিত।
also: invariant
তিন ধাপে প্রমাণ — আর এটা আসলে ছদ্মবেশী [[induction]]:
| ধাপ | Induction-এ সমতুল্য |
|---|---|
| Initialization — loop শুরুর আগে সত্য | base case |
| Maintenance — এক iteration-এ সত্য থাকে | inductive step |
| Termination — loop শেষে যা দাঁড়ায় তাই লক্ষ্য | conclusion |
find_max-এর invariant:
(∀k)(0 ≤ k < i → A[k] ≤ max) ∧ (∃k)(0 ≤ k < i ∧ A[k] == max)দুইটা অংশই দরকার। প্রথমটা ছাড়া max খুব ছোট হতে পারত;
দ্বিতীয়টা ছাড়া max = INT_MAX করে দিলেও প্রথম শর্ত মানত।
Invariant লেখার আসল মূল্য: শুধু “কাজ করে” প্রমাণ করা নয়,
বরং কোন শর্তে কাজ করে সেটা স্পষ্ট করা। find_max-এর
initialization step A[0] পড়ে — তাই precondition n ≥ 1 লাগে।
Testing-এ এই edge case ভুলে যাওয়া যায়; proof-এ যায় না।
কোডে assertion হিসেবে লিখে রাখা যায়:
for i in range(1, len(A)):
if A[i] > m: m = A[i]
assert all(A[k] <= m for k in range(i+1))