Program-এর সঠিকতা — loop invariant আর Hoare logic-এর ধারণা

১ · “চলছে” থেকে “ঠিক” — specification, partial আর total correctness

বাজারঘরের গুদামে প্রতিদিন a-টি অর্ডারের প্যাকেট আসে। একটি ডেলিভারি ভ্যানে ঠিক b-টি প্যাকেট ধরে। ম্যানেজার জানতে চান কয়টি ভ্যান পুরো ভরবে (q) আর কয়টি প্যাকেট পড়ে থাকবে (r). একজন প্রোগ্রামার দুই লাইনের একটি লুপ লিখলেন: যতক্ষণ বাকি প্যাকেট অন্তত b, ততক্ষণ আরেকটি ভ্যান ভরা হবে। কুড়িটি সংখ্যায় চালিয়ে দেখলেন উত্তর মিলছে। প্রশ্ন হলো, এটি কি সব a আর b-এর জন্য ঠিক? আর “ঠিক” কথাটির মানেই বা কী?

আগের পাঁচটি পর্বে প্রমাণ লেখা শিখেছেন: direct, contrapositive, contradiction (পর্ব ০৮), case আর counterexample (পর্ব ০৯), induction (পর্ব ১০), strong induction আর well-ordering (পর্ব ১১), recursive সংজ্ঞা আর structural induction (পর্ব ১২)। এই পর্বে সেই সব হাতিয়ার একটি নতুন ধরনের বস্তুর ওপর প্রয়োগ করব: প্রোগ্রাম. DSA কোর্সের পর্ব ৩ অ্যালগরিদমের দিক থেকে (insertion sort, binary search) এই কাজ দেখায়; এখানে আমরা তার নিচের যুক্তির কাঠামো দেখব, যাতে যেকোনো ছোট প্রোগ্রামের প্রমাণ নিজে লিখতে পারেন।

ভ্যানের সমস্যায়: P = “a ≥ 0 এবং b > 0”, Q = “a = qb + r এবং 0 ≤ r < b”. খেয়াল করুন, Q-তে দুটি অংশই লাগে। শুধু a = qb + r লিখলে q = 0, r = a-ও Q মানত, যা কোনো কাজের উত্তর নয়। আর P-তে b > 0 না থাকলে কী হয়, তা §৬-এ দেখবেন: b = 0 হলে লুপ কখনো থামে না। Specification লেখাই প্রায়ই সবচেয়ে কঠিন অংশ, আর বাস্তবের অনেক বাগ আসলে specification-এর ভুল।

Partial correctness অদ্ভুত শোনাতে পারে: যে প্রোগ্রাম কখনো থামে না, সে যেকোনো Q-এর সাপেক্ষে partially correct, কারণ “থামলে Q” বাক্যটির শর্ত মিথ্যা; পর্ব ০২-এর vacuous truth. তবু দুটি আলাদা রাখার কারণ আছে: দুটি প্রমাণের কৌশল আলাদা। Q-এর প্রমাণ আসে invariant থেকে (§৪), থামার প্রমাণ আসে একটি কমতে থাকা সংখ্যা থেকে (§৬)। আলাদা আলাদা করলে প্রতিটি অংশ ছোট হয়।

২ · Hoare triple আর assignment-এর নিয়ম — পেছন থেকে ভাবা

১৯৬৯ সালে Tony Hoare একটি ছোট সংকেত প্রস্তাব করেন, যা আজ তাঁর নামেই পরিচিত। একটি Hoare triple লেখা হয় {P} S {Q}: “P সত্য অবস্থায় S শুরু করলে, আর S থামলে, শেষে Q সত্য।” অর্থাৎ Hoare triple মানেই partial correctness. বাক্যগুলো (P, Q) পর্ব ০৪-এর predicate: প্রোগ্রামের variable-গুলোর ওপর শর্ত। আর {P} S {Q} প্রমাণের নিয়মগুলোর সংকলনকে বলে Hoare logic. নিয়মগুলো পর্ব ০৬-এর inference rule-এর মতোই লেখা হয়: দাগের ওপরে যা জানা, নিচে যা পাওয়া যায়।

সবচেয়ে ছোট নিয়ম: assignment

x := e মানে “e-এর মান হিসাব করে x-এ রাখা” (Python-এ x = e). প্রশ্ন: এর পরে Q সত্য হতে হলে আগে কী সত্য থাকতে হবে? উত্তর আশ্চর্য রকম সরল: Q-তে যেখানে যেখানে x আছে, সেখানে e বসিয়ে যা পাওয়া যায়। এই বাক্যকে লেখা হয় Q[e/x] (“Q, যেখানে x-এর জায়গায় e”).

কেন পেছন থেকে? কারণ assignment-এর পরে x-এর নতুন মান ঠিক e-এর পুরোনো মান। তাই “পরে x সম্পর্কে Q” আর “আগে e সম্পর্কে Q” একই কথা। সামনে থেকে ভাবতে গেলে বিপদ: {x = 5} x := x + 1 {?}-এর উত্তর “x = 5 আর x = x + 1” লিখলে ভুল, কারণ দুই x আলাদা সময়ের। সামনে থেকে সঠিক নিয়মও আছে (পুরোনো মানের জন্য একটি নতুন নাম লাগে), কিন্তু পেছনের নিয়মটি অনেক পরিষ্কার।

জোড়া লাগানো আর শর্ত শিথিল করা

এই তিনটি নিয়ম দিয়ে যেকোনো assignment-এর ক্রমের প্রমাণ একটি যান্ত্রিক কাজ: শেষ থেকে শুরু করে প্রতিটি assignment পেরোনোর সময় substitution, আর শুরুতে পৌঁছে যে বাক্য পাওয়া যায় তাকে বলে weakest precondition, wp(S, Q): সবচেয়ে দুর্বল শর্ত, যা S-এর পরে Q নিশ্চিত করে। শেষে দেখাতে হয় P ⇒ wp(S, Q); এই গাণিতিক বাক্যটিকে বলে verification condition (VC). প্রোগ্রাম অদৃশ্য হয়ে গেল, রইল শুধু একটি সাধারণ গাণিতিক দাবি, যা আগের পর্বগুলোর পদ্ধতিতে প্রমাণ করা যায়।

1{x = A ∧ y = B}2t := x3x := y4y := t5{x = B ∧ y = A}

এখন একটি ভুল ক্রম ভাবুন: x := y; t := x; y := t. পেছন থেকে গেলে wp দাঁড়ায় y = B ∧ y = A, যা শুধু A = B হলে সত্য; তাই VC মিথ্যা, আর প্রোগ্রামটি ভুল। নিচের ব্লকে একটি ছোট VC generator আছে: এটি assignment-এর তালিকা থেকে পেছন দিকে substitution করে wp ছাপে, তারপর ছোট একটি ক্ষেত্রে প্রতিটি অবস্থায় P ⇒ wp brute force-এ পরীক্ষা করে। প্রথমবার চালালে ব্রাউজারে Python (Pyodide) নামতে কয়েক সেকেন্ড লাগে।

import re
from itertools import product

def subst(cond, var, expr):            # Q[expr/var]: every whole-word var -> (expr)
    return re.sub(rf"\b{var}\b", f"({expr})", cond)

def wp(prog, post):                    # assignments, read from the last one back
    for var, expr in reversed(prog):
        post = subst(post, var, expr)
        print(f"   wp before {var} = {expr:<7}:  {post}")
    return post

def check(title, pre, prog, post, names, dom=range(-3, 4)):
    print(title)
    w = wp(prog, post)
    states = [dict(zip(names, v)) for v in product(dom, repeat=len(names))]
    bad = next((s for s in states if eval(pre, {}, s) and not eval(w, {}, s)), None)
    print(f"   pre => wp on {len(states)} states:", "valid" if bad is None else f"FAILS at {bad}")

check("1) swap with t", "x == A and y == B",
      [("t", "x"), ("x", "y"), ("y", "t")], "x == B and y == A", "xytAB")
check("2) wrong order", "x == A and y == B",
      [("x", "y"), ("t", "x"), ("y", "t")], "x == B and y == A", "xytAB")
check("3) pre x > 6", "x > 6", [("x", "2*x + 1"), ("y", "x - 3")], "y > 10", "xy",
      dom=range(-50, 51))
check("4) pre x >= 6", "x >= 6", [("x", "2*x + 1"), ("y", "x - 3")], "y > 10", "xy",
      dom=range(-50, 51))

1) swap with t
   wp before y = t      :  x == B and (t) == A
   wp before x = y      :  (y) == B and (t) == A
   wp before t = x      :  (y) == B and ((x)) == A
   pre => wp on 16807 states: valid
2) wrong order
   wp before y = t      :  x == B and (t) == A
   wp before t = x      :  x == B and ((x)) == A
   wp before x = y      :  (y) == B and (((y))) == A
   pre => wp on 16807 states: FAILS at {'x': -3, 'y': -2, 't': -3, 'A': -3, 'B': -2}
3) pre x > 6
   wp before y = x - 3  :  (x - 3) > 10
   wp before x = 2*x + 1:  ((2*x + 1) - 3) > 10
   pre => wp on 10201 states: valid
4) pre x >= 6
   wp before y = x - 3  :  (x - 3) > 10
   wp before x = 2*x + 1:  ((2*x + 1) - 3) > 10
   pre => wp on 10201 states: FAILS at {'x': 6, 'y': -50}

৩ · শর্ত আর লুপের নিয়ম — if আর while

প্রোগ্রামে শুধু assignment থাকে না; থাকে if আর while. দুটির জন্য দুটি নিয়ম, আর এই পাঁচটি নিয়মই একটি ছোট প্রোগ্রামিং ভাষার পুরো Hoare logic.

Conditional-এর একটি সম্পূর্ণ প্রমাণ

বাজারঘরে একজন ক্রেতার কাছে দুটি কুপন, ছাড় c₁ আর c₂ টাকা। নিয়ম: বড়টি দেওয়া হবে। প্রোগ্রাম: if c1 ≥ c2 then m := c1 else m := c2. Specification: P = true (কোনো শর্ত নেই), Q = (m ≥ c₁ ∧ m ≥ c₂ ∧ (m = c₁ ∨ m = c₂)). শেষ অংশটি না থাকলে m = ১০ লাখ টাকাও Q মানত; §৮-এ এই ধরনের “দুর্বল specification”-এর বিপদ দেখবেন।

প্রমাণ:

1. প্রথম শাখা: assignment axiom অনুযায়ী wp(m := c₁, Q) = (c₁ ≥ c₁ ∧ c₁ ≥ c₂ ∧ (c₁ = c₁ ∨ c₁ = c₂)), যা সরল করলে c₁ ≥ c₂. — assignment axiom, সরলীকরণ
2. এই শাখায় P ∧ B = (c₁ ≥ c₂), যা ঠিক wp-এর সমান; তাই {P ∧ B} m := c₁ {Q}. — consequence
3. দ্বিতীয় শাখা: wp(m := c₂, Q) সরল করলে c₂ ≥ c₁. — assignment axiom
4. এই শাখায় P ∧ ¬B = (c₁ < c₂), যা থেকে c₂ ≥ c₁ আসে; তাই {P ∧ ¬B} m := c₂ {Q}. — consequence
5. দুই শাখা মিলিয়ে {P} if … {Q}. ∎ — conditional rule

While rule কেন সঠিক: এটি আসলে induction

While rule-এর মধ্যে কোনো জাদু নেই। ধরুন I শুরুতে সত্য, আর প্রতিটি ঘোরা (B সত্য থাকা অবস্থায় S একবার) I রক্ষা করে। দাবি: k-টি ঘোরার পরে I সত্য, প্রতিটি স্বাভাবিক সংখ্যা k-এর জন্য। এটি পর্ব ১০ “Mathematical induction — এক ধাপ থেকে অসীম পর্যন্ত”-এর হুবহু কাঠামো: basis k = 0 (শুরুতে I), inductive step k থেকে k + 1 ({I ∧ B} S {I})। লুপ থামে ঠিক তখন, যখন B মিথ্যা হয়; তখনও I সত্য, তাই শেষে I ∧ ¬B. invariant হলো সেই induction-এর hypothesis, আর ঘোরার সংখ্যা হলো k.

৪ · Loop invariant — ভ্যানের ভাগ আর দিনের মোট বিক্রি

While rule একটি প্রশ্ন রেখে যায়: I কোথা থেকে আসবে? নিয়ম নিজে বলে না; invariant খুঁজে বের করা মানুষের কাজ, আর এটিই প্রোগ্রামের প্রমাণের সৃজনশীল অংশ। একবার I পেলে বাকিটা প্রায় যান্ত্রিক: তিনটি দায় (ছবি ১.১)।

প্রমাণ খুঁজে পাওয়া: আগে খসড়া

ভ্যানের লুপটি a = 17, b = 5-এ হাতে চালাই: (q, r) = (0, 17), (1, 12), (2, 7), (3, 2). প্রতিটি সারিতে 5q + r হিসাব করুন: 17, 17, 17, 17. বদলাচ্ছে q আর r, কিন্তু 5q + r বদলায় না। এটিই invariant-এর গন্ধ: যে রাশি লুপ জুড়ে স্থির থাকে। শেষ অবস্থায় r = 2 < 5, আর 17 = 5 · 3 + 2, ঠিক Q. তাই প্রথম অনুমান I = (a = qb + r). §৭-এ দেখবেন, এই অনুমান একটু দুর্বল; Q-এর 0 ≤ r অংশ পেতে r ≥ 0-ও I-তে রাখতে হয়।

প্রমাণ: invariant I = (a = qb + r ∧ r ≥ 0).

1. Initialization: q := 0; r := a-এর পরে I-এর জন্য wp হলো a = 0 · b + a ∧ a ≥ 0, অর্থাৎ a ≥ 0, যা P থেকে আসে। — assignment axiom, composition, consequence
2. Preservation: ধরি I আর B (r ≥ b) সত্য। Body-র পরে নতুন মান q′ = q + 1, r′ = r − b. তাহলে q′b + r′ = qb + b + r − b = qb + r = a. — I-এর প্রথম অংশ, বীজগণিত
3. আর r′ = r − b ≥ 0, কারণ r ≥ b. তাই body-র পরে আবার I. — B
4. While rule অনুযায়ী লুপ থামলে I ∧ ¬(r ≥ b), অর্থাৎ a = qb + r ∧ r ≥ 0 ∧ r < b. — while rule
5. Exit: এটি হুবহু Q. — consequence
6. Termination: r ≥ 0 সবসময় (I থেকে), আর প্রতি ঘোরায় r অন্তত 1 কমে, কারণ b ≥ 1. অঋণাত্মক পূর্ণসংখ্যা চিরকাল কমতে পারে না (well-ordering, §৬)। তাই লুপ থামে, সর্বোচ্চ a-টি ঘোরায়। ∎

লক্ষ করুন b > 0 কোথায় লেগেছে: শুধু termination-এ। a ≥ 0 লেগেছে initialization-এ। Precondition-এর প্রতিটি অংশ প্রমাণের কোনো না কোনো ধাপে ব্যবহার হওয়া উচিত; কোনো অংশ কোথাও না লাগলে হয় সেটি অপ্রয়োজনীয়, নয়তো প্রমাণে কিছু বাদ পড়েছে।

দ্বিতীয় উদাহরণ: দিনের মোট বিক্রি

বাজারঘরের দিনের n-টি অর্ডারের টাকা একটি অ্যারে A[0], …, A[n − 1]-এ আছে। প্রোগ্রাম: s := 0; i := 0; while i < n do (s := s + A[i]; i := i + 1). P = (n ≥ 0), Q = (s = A[0] + ⋯ + A[n − 1]). Invariant খোঁজার একটি কার্যকর কৌশল: Q-এর একটি ধ্রুবককে লুপের variable দিয়ে বদলান। Q-তে n-এর জায়গায় i বসালে পাই I = (s = A[0] + ⋯ + A[i − 1] ∧ 0 ≤ i ≤ n); i = 0 হলে যোগফল ফাঁকা, মান 0.

1. Initialization: s = 0, i = 0: ফাঁকা যোগফল 0, আর 0 ≤ 0 ≤ n কারণ n ≥ 0. — P
2. Preservation: I আর i < n ধরে s′ = s + A[i] = A[0] + ⋯ + A[i], i′ = i + 1, তাই s′ = A[0] + ⋯ + A[i′ − 1]; আর i < n থেকে i′ ≤ n. — বীজগণিত
3. Exit: I ∧ ¬(i < n) থেকে i ≤ n আর i ≥ n, তাই i = n, আর s = A[0] + ⋯ + A[n − 1] = Q. — consequence
4. Termination: variant n − i: I থেকে ≥ 0, প্রতি ঘোরায় ঠিক 1 কমে। ∎

ধাপ ৩-এ 0 ≤ i ≤ n অংশটি অপরিহার্য: শুধু s-এর অংশ থাকলে “i ≥ n” থেকে i = n বের করা যেত না। Invariant-এ প্রায়ই এমন “সীমার” অংশ লাগে, যা মূল দাবির মতো আকর্ষণীয় নয় কিন্তু exit ধাপটি খাটায়।

প্রমাণকে কোডের পাহারাদার বানানো

Invariant জানা থাকলে তাকে কোডের ভেতরে assertion হিসেবে বসানো যায়: Python-এর assert শর্ত শর্তটি মিথ্যা হলে AssertionError তোলে। প্রতিটি ঘোরায় invariant পরীক্ষা হলে একটি ভুল যেখানে ঘটে, ঠিক সেখানেই ধরা পড়ে, চূড়ান্ত উত্তর ভুল হওয়া পর্যন্ত অপেক্ষা করতে হয় না। নিচের ব্লক ভাগের লুপ আর §৫-এর দ্রুত ঘাতের লুপকে হাজার হাজার এলোমেলো ইনপুটে invariant-সহ চালায়, তারপর দ্রুত ঘাতের একটি ভুল সংস্করণ (b-কে এক লাইন আগে বর্গ করা) চালিয়ে দেখায় invariant কীভাবে বাগ ধরে।

import random
random.seed(13)

def divide(a, b):                      # pre: a >= 0, b > 0
    q, r = 0, a
    while r >= b:
        assert a == q * b + r and r >= 0          # invariant I
        q, r = q + 1, r - b
    assert a == q * b + r and 0 <= r < b          # post Q
    return q, r

def power(a, n, buggy=False):          # pre: n >= 0
    r, b, e = 1, a, n
    while e > 0:
        assert r * b ** e == a ** n, (a, n, r, b, e)   # invariant I
        if buggy:
            b = b * b                  # bug: b squared too early
        if e % 2 == 1:
            r = r * b
        if not buggy:
            b = b * b
        e = e // 2
    return r

cases = [(random.randint(0, 10**5), random.randint(1, 999)) for _ in range(3000)]
print("divide:", all(divide(a, b) == divmod(a, b) for a, b in cases), "on", len(cases), "inputs")
pairs = [(random.randint(-9, 9), random.randint(0, 60)) for _ in range(3000)]
print("power :", all(power(a, n) == a ** n for a, n in pairs), "on", len(pairs), "inputs")
for a, n in [(2, 0), (2, 1), (3, 13)]:
    try:
        print(f"buggy power({a}, {n}) =", power(a, n, buggy=True))
    except AssertionError as err:
        print(f"buggy power({a}, {n}): invariant broken at (a, n, r, b, e) =", err)

divide: True on 3000 inputs
power : True on 3000 inputs
buggy power(2, 0) = 1
buggy power(2, 1) = 4
buggy power(3, 13): invariant broken at (a, n, r, b, e) = (3, 13, 9, 9, 6)

৫ · দ্রুত ঘাত — 3¹³ চার ধাপে

aⁿ হিসাব করার সরল পথ n − 1টি গুণ। কিন্তু 3¹³-এর জন্য বারোটি গুণ লাগে না। 13-এর binary রূপ 1101, অর্থাৎ 13 = 8 + 4 + 1, তাই 3¹³ = 3⁸ · 3⁴ · 3¹; আর 3, 3², 3⁴, 3⁸ পরপর বর্গ করে পাওয়া যায়। এই কৌশলের নাম binary exponentiation (দ্রুত ঘাত)। বড় সংখ্যার modular ঘাতে, যেমন RSA-তে, এটি অপরিহার্য; সেই প্রয়োগ পর্ব ২২ “Modular arithmetic — ঘড়ির গণিত আর modular exponentiation”-এ। এখানে প্রশ্ন শুধু: লুপটি কেন ঠিক?

খসড়া: invariant খুঁজতে জিজ্ঞেস করুন, কোন রাশি স্থির থাকে? r বাড়ে, b বাড়ে, e কমে। “যা হিসাব করা হয়ে গেছে” (r) আর “যা বাকি” (b^e) মিলে সবসময় পুরো উত্তর: I = (r · b^e = aⁿ ∧ e ≥ 0).

প্রমাণ:

1. Initialization: r = 1, b = a, e = n: 1 · aⁿ = aⁿ, আর e = n ≥ 0. — P
2. Preservation, e জোড়: e = 2k ধরি (k ≥ 1). নতুন মান r′ = r, b′ = b², e′ = k. তাহলে r′ · b′^e′ = r · (b²)^k = r · b^2k = r · b^e = aⁿ. — ঘাতের নিয়ম, I
3. Preservation, e বিজোড়: e = 2k + 1 (k ≥ 0). নতুন মান r′ = r · b, b′ = b², e′ = ⌊(2k + 1)/2⌋ = k. তাহলে r′ · b′^e′ = r · b · b^2k = r · b^2k+1 = aⁿ. দুই ক্ষেত্রেই e′ ≥ 0. — proof by cases (পর্ব ০৯)
4. Exit: I ∧ ¬(e > 0) থেকে e ≥ 0 আর e ≤ 0, তাই e = 0, আর r · b⁰ = r = aⁿ. — consequence
5. Termination: variant e. e ≥ 1 হলে ⌊e/2⌋ < e, আর e ≥ 0 সবসময়। ∎

কতবার ঘোরে? প্রতি ঘোরায় e-এর binary রূপের শেষ অঙ্কটি মুছে যায়, তাই n ≥ 1 হলে ঠিক ⌊log₂ n⌋ + 1 বার, অর্থাৎ n-এর binary অঙ্কের সংখ্যা। n = 13-এ 4 বার, n = 10¹⁸-এও মাত্র 60 বার।

1r, b, e = 1, 3, 132while e > 0:3  if e % 2 == 1: r = r*b4  b = b * b5  e = e // 26# e = 0: r = 3^13

৬ · লুপ থামবে তো? — variant আর Euclid-এর gcd

Partial correctness প্রমাণ হয়ে গেলেও একটি প্রশ্ন বাকি: termination, অর্থাৎ লুপ কি সত্যিই থামবে? এর সাধারণ হাতিয়ার একটি variant function: প্রোগ্রামের variable থেকে হিসাব করা একটি পূর্ণসংখ্যা V, যা

• লুপ চলাকালীন কখনো ঋণাত্মক হয় না (I ∧ B ⇒ V ≥ 0), এবং
• প্রতিটি ঘোরায় কঠোরভাবে কমে (body-র পরের V < আগের V).

প্রমাণ (contradiction):

1. ধরি লুপ কখনো থামে না; তাহলে প্রতিটি k-এর জন্য k-তম ঘোরা আছে, আর V-এর মানের অসীম ক্রম V₀ > V₁ > V₂ > ⋯ পাই। — দ্বিতীয় শর্ত
2. প্রতিটি V_k ≥ 0, তাই সেট {V₀, V₁, …} স্বাভাবিক সংখ্যার একটি অশূন্য উপসেট। — প্রথম শর্ত
3. Well-ordering principle অনুযায়ী এর একটি ক্ষুদ্রতম উপাদান V_m আছে। — well-ordering (পর্ব ১১)
4. কিন্তু V_m+1 < V_m, আর V_m+1-ও সেটে আছে; ক্ষুদ্রতমের চেয়েও ছোট উপাদান, বিরোধ। ∎

এটি পর্ব ১১ “Strong induction আর well-ordering”-এর minimal counterexample কৌশলেরই আরেক রূপ। আর সীমাটি সহজ: পূর্ণসংখ্যা প্রতিবার অন্তত 1 কমলে V₀-এর পরে বড়জোর V₀ ধাপে 0-তে পৌঁছায়।

Euclid-এর gcd: invariant আর variant একসঙ্গে

দুটি অঋণাত্মক পূর্ণসংখ্যার gcd (গরিষ্ঠ সাধারণ গুণনীয়ক) বের করার Euclid-এর algorithm প্রায় ২,৩০০ বছর পুরোনো: x := a; y := b; while y ≠ 0 do (x, y := y, x mod y). বাজারঘরের উদাহরণ: ১০৭১টি সাবান আর ৪৬২টি টুথপেস্ট সমান সংখ্যক প্যাকেটে, প্রতিটি প্যাকেটে একই মিশ্রণে ভাগ করতে চাইলে সর্বোচ্চ কয়টি প্যাকেট? উত্তর gcd(1071, 462) = 21. সংখ্যাতত্ত্বের দিক (Bézout, extended Euclid) পর্ব ২১ “GCD আর Euclid-এর algorithm — Bézout আর extended Euclid”-এ; recursive রূপের induction-প্রমাণ DSA কোর্সের পর্ব ৩-এ। এখানে লুপ রূপের প্রমাণ।

প্রমাণ:

1. ভাগের উপপাদ্য (উপপাদ্য ৪.১-এর লুপ ঠিক এটিই হিসাব করে): x = qy + m, যেখানে m = x mod y. — division algorithm
2. (⇒) d ∣ x আর d ∣ y হলে x = dk₁, y = dk₂; তাহলে m = x − qy = d(k₁ − qk₂), আর k₁ − qk₂ ∈ ℤ, তাই d ∣ m. — বীজগণিত, closure
3. (⇐) d ∣ y আর d ∣ m হলে y = dk₂, m = dk₃; তাহলে x = qy + m = d(qk₂ + k₃), তাই d ∣ x. ∎ — বীজগণিত

প্রমাণ: invariant I = “(x, y)-এর সাধারণ ভাজকের সেট = (a, b)-এর সাধারণ ভাজকের সেট, x ≥ 0, y ≥ 0, (x, y) ≠ (0, 0)”.

1. Initialization: x = a, y = b, তাই সেট দুটি একই; বাকি অংশ P থেকে। — P
2. Preservation: y ≠ 0, তাই y > 0; লেমা ৬.২ বলে (y, x mod y)-এর সাধারণ ভাজক = (x, y)-এর সাধারণ ভাজক = (a, b)-এর। নতুন জোড়া (y, x mod y)-এ y > 0, তাই (0, 0) নয়, আর 0 ≤ x mod y. — লেমা ৬.২
3. Exit: y = 0 হলে (x, 0)-এর সাধারণ ভাজক মানে x-এর ভাজক (সবকিছু 0-কে ভাগ করে), আর x > 0. x-এর সবচেয়ে বড় ভাজক x নিজে, তাই gcd(a, b) = x. — I ∧ ¬B
4. Termination: variant y. লুপে y ≥ 0, আর নতুন y = x mod y, যা 0 ≤ x mod y < y. উপপাদ্য ৬.১ প্রয়োগ। ∎

1x, y = 1071, 4622while y != 0:3  x, y = y, x % y4# y = 0: x = gcd

সীমা কতটা টাইট? নিচের ব্লক ৩০০ পর্যন্ত সব জোড়ায় ঘোরার সংখ্যা গোনে, আর দেখায় variant না থাকলে কী হয়: b = 0 বা b < 0 হলে ভাগের লুপ, আর একটি “2 করে কমা” লুপ, যার “variant” আসলে নিচে আটকায় না।

def euclid(x, y):                     # pre: x >= 0, y >= 0
    variant = [y]                     # values of the variant y
    while y != 0:
        x, y = y, x % y
        variant.append(y)
    return x, variant

print("gcd(1071, 462):", euclid(1071, 462))

# how many rounds at most? search all pairs 1 <= y < x <= 300
worst = max(((len(euclid(x, y)[1]) - 1, x, y)
             for x in range(2, 301) for y in range(1, x)))
print("most rounds for x <= 300:", worst)

def divide(a, b, cap=8):              # the division loop, with a safety cap
    q, r, rounds = 0, a, 0
    while r >= b:
        q, r, rounds = q + 1, r - b, rounds + 1
        if rounds == cap:
            return f"still running after {cap} rounds (r = {r})"
    return q, r

for a, b in [(17, 5), (17, 0), (17, -3)]:
    print(f"divide({a}, {b}):", divide(a, b))

def countdown(x, cap=6):              # pre: x >= 0 ... but is x a good variant?
    seen = [x]
    while x != 0 and len(seen) < cap:
        x = x - 2
        seen.append(x)
    return seen

print("countdown(6):", countdown(6), " countdown(5):", countdown(5))

gcd(1071, 462): (21, [462, 147, 21, 0])
most rounds for x <= 300: (11, 233, 144)
divide(17, 5): (3, 2)
divide(17, 0): still running after 8 rounds (r = 17)
divide(17, -3): still running after 8 rounds (r = 41)
countdown(6): [6, 4, 2, 0]  countdown(5): [5, 3, 1, -1, -3, -5]

৭ · যন্ত্রে যাচাই — Z3 দিয়ে verification condition

§২-এর VC generator ছোট পরিসরে brute force করেছিল। একটি SMT solver একই VC সব পূর্ণসংখ্যার জন্য পরীক্ষা করতে পারে: VC-এর অস্বীকার ¬VC-কে সত্য করে এমন কোনো মান নেই দেখালেই VC প্রমাণিত; থাকলে সেই মানগুলোই একটি counterexample. পর্ব ০৭-এ Z3 দিয়ে কুপন-নিয়ম যাচাই দেখেছেন; এবার একে প্রোগ্রামের প্রমাণে লাগাব। প্রোগ্রাম থেকে VC বানিয়ে solver-কে দেওয়া, এটিই আধুনিক formal verification টুলের (যেমন Dafny, Why3, Frama-C) মূল কাঠামো।

নিচের পরীক্ষাগুলো এই কোর্সের লেখার সময় একটি সাধারণ Windows ডেস্কটপে সত্যিকারভাবে চালানো হয়েছে: Python 3.12, z3-solver 5.3.3 (MIT লাইসেন্স), uv দিয়ে বানানো একটি ছোট প্রজেক্টে। নিজের কম্পিউটারে চালাতে চাইলে:

cd ~/bazarghar-dm
uv add z3-solver
uv run python hoare_swap.py
uv run python div_vc.py
uv run python gcd_vc.py

সত্যিকারের run ১: swap, Hoare logic-এ

Z3-এর substitute ঠিক assignment axiom-এর Q[e/x]. তাই wp লেখার ফাংশন তিন লাইনের:

from z3 import Ints, BitVecs, And, Implies, substitute, prove

def wp(prog, post):
    # weakest precondition of a list of assignments (var, expr):
    # go backwards, replacing var by expr in the postcondition
    for var, expr in reversed(prog):
        post = substitute(post, (var, expr))
    return post

def check(name, pre, prog, post):
    vc = Implies(pre, wp(prog, post))
    print(f"{name:22}", end=" ")
    prove(vc)

x, y, t, A, B = Ints("x y t A B")
pre, post = And(x == A, y == B), And(x == B, y == A)

check("swap with temp", pre, [(t, x), (x, y), (y, t)], post)
check("swap, wrong order", pre, [(x, y), (t, x), (y, t)], post)
check("swap by + and -", pre, [(x, x + y), (y, x - y), (x, x - y)], post)

# same arithmetic trick on 8-bit machine integers (wrap-around)
bx, by, bA, bB = BitVecs("bx by bA bB", 8)
check("8-bit swap by + and -", And(bx == bA, by == bB),
      [(bx, bx + by), (by, bx - by), (bx, bx - by)], And(bx == bB, by == bA))

$ uv run python hoare_swap.py
swap with temp         proved
swap, wrong order      counterexample
[B = 1, A = 0, x = 0, y = 1]
swap by + and -        proved
8-bit swap by + and -  proved

প্রথম দুটি §২-এর ফলই, তবে এবার সব পূর্ণসংখ্যার জন্য: সঠিক ক্রম “proved”, ভুল ক্রমে A = 0, B = 1 counterexample. তৃতীয়টি একটি পুরোনো কৌশল, t ছাড়াই swap: x := x + y; y := x − y; x := x − y. গণিতের পূর্ণসংখ্যায় এটি সঠিক। চতুর্থটি আরও মজার: ৮-bit যন্ত্র-পূর্ণসংখ্যায় (BitVec, যেখানে 255 + 1 = 0, অর্থাৎ mod 256 গণিত) যোগফল উপচে পড়লেও উত্তর ঠিক থাকে, কারণ mod 256-এ যোগ-বিয়োগ একে অপরকে বাতিল করে। Z3 দুটি জগতকে আলাদাভাবে যুক্তি করতে পারে; প্রোগ্রামের প্রমাণে কোন জগৎ (গণিতের ℤ, না যন্ত্রের সীমিত bit) তা স্পষ্ট বলা জরুরি।

সত্যিকারের run ২: ভাগের লুপের চারটি VC

§৪-এর তিন দায় আর termination, চারটি আলাদা VC. দুটি invariant দিয়ে চালাই: সঠিকটি, আর §৪-এর খসড়ার প্রথম অনুমান (r ≥ 0 ছাড়া)।

from z3 import Ints, IntVal, And, Not, Implies, Solver, substitute, unsat

# q = 0; r = a;  while r >= b: q = q + 1; r = r - b
a, b, q, r = Ints("a b q r")
pre   = And(a >= 0, b > 0)
guard = r >= b
post  = And(a == q * b + r, 0 <= r, r < b)

def before_loop(e):  return substitute(e, (q, IntVal(0)), (r, a))
def after_body(e):   return substitute(e, (q, q + 1), (r, r - b))

def vcs(inv):
    return {"1 init    ": Implies(pre, before_loop(inv)),
            "2 preserve": Implies(And(pre, inv, guard), after_body(inv)),
            "3 exit    ": Implies(And(pre, inv, Not(guard)), post),
            "4 variant ": Implies(And(pre, inv, guard),
                                  And(after_body(r) < r, after_body(r) >= 0))}

for name, inv in [("a == q*b + r and r >= 0", And(a == q * b + r, r >= 0)),
                  ("a == q*b + r (weaker)  ", a == q * b + r)]:
    print("invariant:", name)
    for vc_name, vc in vcs(inv).items():
        s = Solver(); s.add(Not(vc))          # valid  <=>  Not(vc) has no model
        print("  ", vc_name, "valid" if s.check() == unsat else f"FAILS {s.model()}")

$ uv run python div_vc.py
invariant: a == q*b + r and r >= 0
   1 init     valid
   2 preserve valid
   3 exit     valid
   4 variant  valid
invariant: a == q*b + r (weaker)
   1 init     valid
   2 preserve valid
   3 exit     FAILS [q = 7, a = 3, b = 13, r = -88]
   4 variant  valid

সঠিক invariant-এ চারটি VC-ই valid: উপপাদ্য ৪.১-এর হাতের প্রমাণ যন্ত্রও মেনে নিল। দুর্বল invariant-এ exit ভাঙে, আর counterexample-টি পড়ার মতো: a = 3, b = 13, q = 7, r = −88. পরীক্ষা করুন: 7 · 13 + (−88) = 91 − 88 = 3, তাই a = qb + r সত্য, আর r = −88 < 13, তাই লুপ থেমেছে; কিন্তু Q-এর 0 ≤ r মিথ্যা। আসল প্রোগ্রামে r কখনো −88 হয় না; সমস্যা হলো দুর্বল invariant সেটি বলে না, তাই প্রমাণ এগোতে পারে না। এটি invariant-এর একটি মৌলিক শিক্ষা: invariant সত্য হওয়াই যথেষ্ট নয়, প্রমাণ চালানোর মতো শক্ত হতে হয়।

সত্যিকারের run ৩: যেখানে solver আটকে যায়

এবার Euclid-এর লেমা ৬.২-এর (⇒) দিক। প্রথমে solver-কে সরাসরি জিজ্ঞেস করি (mod দিয়ে), তারপর মানুষের প্রমাণের ইঙ্গিত (m = d(k₁ − qk₂)) দিয়ে। ফাইলের মূল অংশ:

x, y, d, q, m, k1, k2, k3 = Ints("x y d q m k1 k2 k3")

def show(name, *facts_and_negated_goal):
    s = Solver(); s.set("timeout", 20000)          # 20 seconds at most
    s.add(*facts_and_negated_goal)
    t0 = time.perf_counter(); res = s.check(); dt = time.perf_counter() - t0
    print(f"{name:34}", "proved" if res == unsat else res, f"({dt:.2f} s)")

show("variant: 0 <= x % y < y", y > 0, Not(And(0 <= x % y, x % y < y)))
show("d|x, d|y => d|(x%y), raw %",
     x >= 0, y > 0, d > 0, x % d == 0, y % d == 0, Not((x % y) % d == 0))
show("same, hint m = d*(k1 - q*k2)",
     x == q * y + m, x == d * k1, y == d * k2, Not(m == d * (k1 - q * k2)))
show("back: x = d*(q*k2 + k3)",
     x == q * y + m, y == d * k2, m == d * k3, Not(x == d * (q * k2 + k3)))

$ uv run python gcd_vc.py
variant: 0 <= x % y < y            proved (0.00 s)
d|x, d|y => d|(x%y), raw %         unknown (20.01 s)
same, hint m = d*(k1 - q*k2)       proved (0.00 s)
back: x = d*(q*k2 + k3)            proved (0.00 s)

Variant-এর VC সঙ্গে সঙ্গে প্রমাণ। কিন্তু লেমার সরাসরি রূপে Z3 বিশ সেকেন্ড চেষ্টা করে বলল unknown: সে প্রমাণও পায়নি, counterexample-ও পায়নি। কারণ এখানে variable-এর সঙ্গে variable-এর গুণ আর mod আছে (অরৈখিক পূর্ণসংখ্যা গণিত), আর এমন সূত্রের সত্যতা সাধারণভাবে কোনো algorithm দিয়েই নির্ধারণ করা যায় না (undecidable; ভাবনার প্রশ্ন ২)। তারপর মানুষ লেমার প্রমাণ থেকে “সাক্ষী” রাশি k₁ − qk₂ লিখে দিল, আর একই দাবি শূন্য সেকেন্ডে প্রমাণ হলো; উল্টো দিকও। সময়ের সংখ্যা যন্ত্রভেদে বদলাবে, কিন্তু শিক্ষাটি বদলাবে না: verifier প্রমাণের যান্ত্রিক অংশ নেয়; invariant বাছাই আর মূল কৌশল (এখানে সাক্ষী) এখনো সাধারণত মানুষকে দিতে হয়। আর unknown মানে কখনোই “প্রমাণিত” নয়।

৮ · Testing বনাম প্রমাণ — আর একটি ভুল প্রমাণ ধরা

এই উক্তিটি সাধারণত ১৯৬৯-৭০ সালের দিকে Dijkstra-র লেখা ও বক্তৃতার (তাঁর “Notes on Structured Programming” সহ) বলে উল্লেখ করা হয়; হুবহু শব্দ উৎসভেদে একটু আলাদা পাওয়া যায়। অর্থ পরিষ্কার: টেস্ট কয়েকটি ইনপুট দেখে, প্রমাণ সবগুলো। পর্ব ০৮-এর ভাষায়, টেস্ট উদাহরণ, প্রমাণ উপপাদ্য। তবে উল্টো দিকটাও সত্য: প্রমাণ শুধু ততটুকু নিশ্চিত করে, যতটুকু specification বলে, আর specification নিজেই ভুল হতে পারে। তাই বাস্তবে দুটি একসঙ্গে চলে। টেস্ট লেখার বিস্তারিত সফটওয়্যার ইঞ্জিনিয়ারিং ও Git কোর্সের পর্ব ৪৫ আর Python কোর্সের পর্ব ৪২-এ।

একটি বাস্তবধর্মী উদাহরণ: পূর্ণসংখ্যার বর্গমূলের পূর্ণ অংশ ⌊√n⌋. দ্রুত উপায় মনে হয় int(math.sqrt(n)); কিন্তু math.sqrt float-এ কাজ করে, যার নির্ভুলতা সীমিত। বিকল্প হলো invariant-সহ binary search: lo² ≤ n < hi², variant hi − lo. এর প্রমাণ §৪-এর ধাঁচেই (অনুশীলনের মতো করে নিজে লিখে দেখতে পারেন)।

import math, random
random.seed(2026)

def isqrt_float(n):                    # quick idea: use the float square root
    return int(math.sqrt(n))

def isqrt_proved(n):                   # pre: n >= 0
    lo, hi = 0, n + 1                  # invariant: lo*lo <= n < hi*hi
    while hi - lo > 1:                 # variant: hi - lo
        mid = (lo + hi) // 2
        if mid * mid <= n:
            lo = mid
        else:
            hi = mid
    return lo                          # post: lo*lo <= n < (lo+1)**2

tests = [random.randrange(10**9) for _ in range(20000)]
agree = all(isqrt_float(n) == isqrt_proved(n) for n in tests)
print("20000 random tests below 10**9, both agree:", agree)

for n in [10**16 - 1, 4503599761588224]:
    f, p = isqrt_float(n), isqrt_proved(n)
    print(f"n = {n}: float gives {f}, proved gives {p}, "
          f"check {p}^2 <= n < {p + 1}^2: {p * p <= n < (p + 1) ** 2}")
print("math.isqrt agrees:", math.isqrt(10**16 - 1), math.isqrt(4503599761588224))

20000 random tests below 10**9, both agree: True
n = 9999999999999999: float gives 100000000, proved gives 99999999, check 99999999^2 <= n < 100000000^2: True
n = 4503599761588224: float gives 67108865, proved gives 67108864, check 67108864^2 <= n < 67108865^2: True
math.isqrt agrees: 99999999 67108864

প্রমাণের ভুল ধরুন: invariant শুরুতেই মিথ্যা

একজন §৪-এর মোট বিক্রির লুপের (s := 0; i := 0; while i < n …) এই “প্রমাণ” লিখলেন। পড়ে ভুলটি নিজে খুঁজুন।

1. Invariant: I = (s = A[0] + ⋯ + A[i]).
2. Preservation: I আর i < n ধরে, body-র পরে s′ = s + A[i]… (বীজগণিত, দেখতে ঠিকঠাক)।
3. Exit: i = n, তাই s = A[0] + ⋯ + A[n]. এটিই মোট বিক্রি। ∎

ভুল কোথায়: initialization ধাপটিই নেই, আর থাকলে ভাঙত: শুরুতে s = 0, অথচ I বলে s = A[0], যা A[0] ≠ 0 হলে মিথ্যা। এটি induction-এ basis বাদ দেওয়ার মতো ভুল (পর্ব ১০-এর “সব ঘোড়ার রং এক” ধাঁচের)। লক্ষণও আছে: exit-এর উত্তরে A[n] এসেছে, যা অ্যারের বাইরে (index 0 থেকে n − 1). আসলে body-র পরে i বাড়ে, তাই preservation-ও এই I-এর জন্য খাটে না। সঠিক invariant §৪-এরটি: s = A[0] + ⋯ + A[i − 1]. Off-by-one ভুল প্রায়ই invariant-এর একটি সূচক ভুল থেকে আসে, আর তিন দায়ের প্রতিটি পরীক্ষা করলে ধরা পড়ে।

৯ · AI-এর যুগে — AI-এর লেখা কোড আর তার “প্রমাণ” যাচাই

AI সহকারী এখন মুহূর্তে লুপ লেখে, আর চাইলে সঙ্গে একটি invariant আর “প্রমাণ”-ও দেয়। সেগুলো দেখতে নিখুঁত, কিন্তু এই পর্বের প্রতিটি ভুল সেখানে নিয়মিত পাওয়া যায়:

AI-এর কোড আর প্রমাণ হাতে পেলে — যাচাইয়ের চেকলিস্ট

• Precondition আর postcondition লেখা আছে, আর postcondition যথেষ্ট শক্ত (যেমন “m ≥ সব”-এর সঙ্গে “m তালিকার একটি”)
• Invariant-এর তিন দায় আলাদা করে পরীক্ষা করেছি; প্রথম ঘোরার আগে I সত্য
• Variant নিচে আটকানো (≥ 0) আর প্রতি ঘোরায় কঠোরভাবে কমে
• কোডে assert বসিয়ে ছোট সব ইনপুটে আর এলোমেলো বড় ইনপুটে চালিয়েছি
• সম্ভব হলে VC-গুলো Z3-এ দিয়েছি, আর “unknown”-কে প্রমাণ ধরিনি
• উল্লেখ করা টুল, উপপাদ্য বা ইতিহাস একটি বিশ্বস্ত পাঠ্যবই বা অফিসিয়াল ডকুমেন্টেশনে মিলিয়েছি

মনে রাখুন, AI-এর লেখা invariant-কে assert বানিয়ে চালানো সবচেয়ে সস্তা প্রথম পরীক্ষা: একবার ভাঙলেই “প্রমাণ” বাতিল। আর ভাঙেনি মানেই প্রমাণিত নয়; তখন তিন দায় নিজে পড়ুন।