সঠিকতা প্রমাণ — লুপ ইনভেরিয়েন্ট ও ইনডাকশন

১ · লুপ ইনভেরিয়েন্ট কী, এবং ইনডাকশনের সাথে সম্পর্ক

একটি অ্যালগরিদম "সঠিক" — এই দাবিটি শুধু কয়েকটি উদাহরণে সঠিক আউটপুট দেখে প্রমাণ করা যায় না (উদাহরণে ঠিক থাকলেও অন্য কোনো ইনপুটে ভুল হতে পারে)। প্রয়োজন একটি সাধারণ (general) প্রমাণ, যা সব বৈধ ইনপুটের জন্য একসাথে কাজ করে। লুপ-ভিত্তিক অ্যালগরিদমের জন্য এই কাজে ব্যবহৃত হয় একটি লুপ ইনভেরিয়েন্টLoop invariantএমন একটি প্রপার্টি (দাবি) যা লুপের প্রতিটি ইটারেশন শুরু হওয়ার আগমুহূর্তে সত্য থাকে — লুপ ঠিক কতবার চলবে তা নির্বিশেষে।।

লুপ ইনভেরিয়েন্ট দিয়ে সঠিকতা প্রমাণ করা গাণিতিক ইনডাকশনের সাথে হুবহু সমান্তরাল — শুধু "$n$-তম ধাপ" এর জায়গায় "লুপের $k$-তম ইটারেশন" বসে:

এই তিনটি ধাপ একসাথে প্রমাণ করে যে ইনভেরিয়েন্টটি লুপের প্রতিটি ইটারেশনের শুরুতে সত্য (Initialization + Maintenance = ইনডাকশন দ্বারা সব ইটারেশনে সত্য), এবং লুপ শেষে এই সত্যতা থেকেই কাঙ্ক্ষিত ফলাফল বেরিয়ে আসে (Termination)।

২ · উদাহরণ অ্যালগরিদম — ইনসার্শন সর্ট

ইনসার্শন সর্ট ইতিমধ্যে DSA কোর্সে কীভাবে কাজ করে ও ইমপ্লিমেন্ট করতে হয় তা কভার করা হয়েছে — এখানে আমরা সরাসরি এর রিগোরাস সঠিকতা প্রমাণে যাচ্ছি। নিচে অ্যালগরিদমের সিউডোকোড দেওয়া হলো (0-ইনডেক্সিং-এ, M1/L02-এর কনভেনশন অনুসরণ করে) — এটি শুধু ব্যাখ্যামূলক টেক্সট, সরাসরি চালানো যায় না:

INSERTION-SORT(A)
  for j ← 1 to length(A) - 1
      key ← A[j]
      i ← j - 1
      while i ≥ 0 and A[i] > key
          A[i + 1] ← A[i]
          i ← i - 1
      A[i + 1] ← key

ধারণাটি সহজ: প্রতিটি ইটারেশনে A[j]-কে "key" হিসেবে ধরা হয়, এবং ইতিমধ্যে সাজানো অংশ $A[0 \,..\, j-1]$-এর মধ্যে key-এর সঠিক অবস্থানে সেটি বসিয়ে দেওয়া হয় (key-এর চেয়ে বড় এলিমেন্টগুলো এক ঘর ডানে সরিয়ে জায়গা করে দেওয়া হয়)।

৩ · ইনভেরিয়েন্ট বিবৃতি

আমরা দাবি করছি:

৪ · Initialization — প্রথম ইটারেশনের আগে

প্রথম ইটারেশন শুরু হয় $j = 1$ দিয়ে। তখন subarray $A[0 \,..\, j-1] = A[0 \,..\, 0]$ — অর্থাৎ একটিমাত্র এলিমেন্ট, $A[0]$। একটিমাত্র এলিমেন্টের যেকোনো ক্রম স্বতঃসিদ্ধভাবেই সাজানো (একটি এলিমেন্টকে অন্য কোনো এলিমেন্টের সাথে তুলনা করার প্রয়োজনই নেই)। সুতরাং ইনভেরিয়েন্টটি প্রথম ইটারেশন শুরুর আগে সত্য। এটাই ইনডাকশনের base case।

৫ · Maintenance — প্রতিটি ইটারেশন ইনভেরিয়েন্ট বজায় রাখে

ধরে নিই ইনভেরিয়েন্টটি কোনো ইটারেশন $j$ শুরুর আগে সত্য — অর্থাৎ $A[0 \,..\, j-1]$ ইতিমধ্যে সাজানো। ইটারেশনের শরীরে কী ঘটে তা দেখা যাক: key ← A[j] নেওয়া হয়, তারপর while লুপ $A[0 \,..\, j-1]$-এর মধ্যে key-এর চেয়ে বড় প্রতিটি এলিমেন্ট এক ঘর ডানে সরায় (যতক্ষণ না key-এর চেয়ে ছোট বা সমান কোনো এলিমেন্ট বা অ্যারের শুরু পাওয়া যায়), এবং শেষে key-কে সেই ফাঁকা জায়গায় বসিয়ে দেয়। যেহেতু $A[0 \,..\, j-1]$ ইতিমধ্যে সাজানো ছিল (ইনডাকটিভ hypothesis অনুযায়ী), key-এর সঠিক অবস্থান একটিই এবং এই শিফটিং প্রক্রিয়া ঠিক সেই অবস্থানেই key-কে বসায়। ফলে ইটারেশন শেষে $A[0 \,..\, j]$ সাজানো থাকে — যা পরের ইটারেশন ($j+1$) শুরুর আগে ঠিক ইনভেরিয়েন্টেরই দাবি। এলিমেন্টগুলোর সেট অপরিবর্তিত থাকে কারণ শুধু শিফট ও একটি বসানো হয়েছে, কোনো এলিমেন্ট হারিয়ে যায়নি বা নতুন যোগ হয়নি। এটাই ইনডাকটিভ স্টেপ।

৬ · Termination — লুপ শেষে

বহিরাগত for লুপটি থামে যখন $j$, $\text{length}(A) - 1$ অতিক্রম করে — অর্থাৎ $j = n$ হয়ে যায় ($n$ = অ্যারের দৈর্ঘ্য)। Initialization ও Maintenance ধাপ দুটো একসাথে (ইনডাকশন দ্বারা) প্রমাণ করে যে ইনভেরিয়েন্টটি $j = n$ হওয়ার মুহূর্তেও সত্য — অর্থাৎ subarray $A[0 \,..\, n-1]$ সাজানো। কিন্তু $A[0 \,..\, n-1]$ মানেই তো পুরো অ্যারে! সুতরাং লুপ শেষ হওয়ার মুহূর্তে সম্পূর্ণ অ্যারেটি সাজানো থাকে — যা প্রমাণ করে ইনসার্শন সর্ট সঠিক। $\blacksquare$

৭ · কোডে প্রমাণ যাচাই — প্রতিটি ইটারেশনে সত্যিকারের assert

উপরের "Maintenance" প্রমাণটি প্রতিবার একটি নির্দিষ্ট দাবি করে: প্রতিটি ইটারেশনের পর, $A[0 \,..\, j]$ সাজানো থাকতে হবে। এই দাবিটি নিছক প্রমাণেই সীমাবদ্ধ না রেখে, নিচের কোডে সত্যিকারের Python assert দিয়ে প্রতিটি ইটারেশনের পর সরাসরি চেক করা হয়েছে — যদি প্রমাণে কোনো ভুল থাকত, নিচের কোডটি কোনো না কোনো ইনপুটে AssertionError দিয়ে ক্র্যাশ করত:

def insertion_sort_with_invariant_check(arr):
    a = arr[:]
    n = len(a)
    checks_passed = 0
    for j in range(1, n):
        key = a[j]
        i = j - 1
        while i >= 0 and a[i] > key:
            a[i + 1] = a[i]
            i -= 1
        a[i + 1] = key

        # --- ইনভেরিয়েন্ট চেক (Maintenance ধাপ, সত্যিকারের assert) ---
        # দাবি: এই ইটারেশনের পর A[0..j] অবশ্যই সাজানো থাকবে
        prefix = a[:j + 1]
        assert prefix == sorted(prefix), f"j={j} এ ইনভেরিয়েন্ট ভঙ্গ হয়েছে!"
        checks_passed += 1

    return a, checks_passed

arr = [5, 2, 9, 1, 5, 6, 3]
sorted_arr, checks = insertion_sort_with_invariant_check(arr)

print("ইনপুট:          ", arr)
print("আউটপুট (সাজানো): ", sorted_arr)
print(f"মোট {checks}টি ইনভেরিয়েন্ট চেক করা হলো — একটিও fail করেনি (assert ব্যতিক্রম ছাড়াই সম্পন্ন)")
print("পাইথনের sorted() এর সাথে মিলছে:", sorted_arr == sorted(arr))