Formal Methods — Hoare Logic, Model Checking, TLA+

Postcondition I: s = (i-1)i/2 ∧ 1 ≤ i ≤ n+1 থেকে শুরু, পেছনের দিকে যাই।

দ্বিতীয় statement (s:=0) -এর জন্য assignment axiom: I-তে s-এর জায়গায় 0 বসাই:

$I[0/s] = \big(0 = (i-1)i/2\big) \wedge 1 \le i \le n+1$

প্রথম statement (i:=1) -এর জন্য assignment axiom: উপরের predicate-এ i-এর জায়গায় 1 বসাই:

$\big(0 = (1-1)\cdot 1/2\big) \wedge 1 \le 1 \le n+1$ $= (0 = 0) \wedge (n \ge 0) = \text{true} \wedge (n \ge 0) = n \ge 0$

তাহলে sequence rule অনুযায়ী:

$\{n \ge 0\}\ \ i:=1;\, s:=0\ \ \{I\}$

ঠিক যা প্রমাণ করতে চেয়েছিলাম। এই একই ফলাফল আমরা lesson-এর মূল টেক্সটে “সামনে থেকে” (i=1, s=0 বসিয়ে সরাসরি চেক করে) পেয়েছিলাম — দুইটা পথই মেলে, কারণ assignment axiom logically সমতুল্য দুইদিকেই প্রয়োগযোগ্য। Backward application (এই উত্তরে) সবসময় নিরাপদ — mechanically প্রয়োগ করা যায়; forward substitution (“বসিয়ে চেক করা”) প্রায়ই দ্রুত কিন্তু সবসময় সরাসরি rule-এর রূপ নয়, rule of consequence প্রয়োজন হতে পারে।

Invariant: I: p = k! ∧ 0 ≤ k ≤ n

এটা postcondition (p = n!)-এর সাধারণীকরণ, ঠিক sum-loop-এর মতো — “এখন পর্যন্ত যতগুলো factor গুণ হয়েছে, p-তে তাদের factorial আছে।”

Initialization: {n ≥ 0} k:=0; p:=1 {I}

I-তে k=0, p=1 বসাই: 1 = 0! = 1 ✓, আর 0 ≤ 0 ≤ n ⟺ n ≥ 0 ✓ — ঠিক precondition। Sequence + assignment axiom দিয়ে formally ধাপে ধাপে: I[1/p][0/k] সরল করলে n ≥ 0 আসে (Question 1-এর মতোই কৌশল)।

Maintenance: {I ∧ k < n} k:=k+1; p:=p*k {I}

পেছন থেকে: I-তে p-এর জায়গায় p*k বসাই না — প্রথমে শেষ statement (p := p*k) থেকে শুরু। I-তে p-এর জায়গায় p*k বসাই:

$I[p{\cdot}k/p] = \big(p \cdot k = k!\big) \wedge 0 \le k \le n$

এবার প্রথম statement (k := k+1) — এই predicate-এ k-এর জায়গায় k+1 বসাই:

$\big(p \cdot (k{+}1) = (k{+}1)!\big) \wedge 0 \le k+1 \le n$

সরলীকরণ: (k+1)! = (k+1)·k!, তাই প্রথম অংশ ⟺ p = k! (যেহেতু k+1 ≠ 0, দুই পাশ ভাগ করা যায়)। দ্বিতীয় অংশ ⟺ -1 ≤ k ≤ n-1।

তাহলে দেখাতে হবে: I ∧ (k < n) ⟹ (p = k! ∧ -1 ≤ k ≤ n-1)

I মানে p = k! (মিলে যায়) আর 0 ≤ k ≤ n, প্লাস k < n মানে 0 ≤ k ≤ n-1 — যা -1 ≤ k ≤ n-1-কে entail করে (দুর্বল করে) ✓ Rule of consequence দিয়ে maintenance প্রমাণিত। ∎

Loop শেষে: I ∧ ¬(k<n) = p=k! ∧ 0≤k≤n ∧ k≥n ⟹ k=n, তাই p = n! — postcondition। ✓

Termination: variant n - k, প্রতি iteration-এ ঠিক ১ কমে, k ≤ n থাকা অবস্থায় অ-ঋণাত্মক — well-ordering দিয়ে সসীম ধাপে থামে।

While rule দিয়ে I = true নিন। {true ∧ true} skip {true} তুচ্ছভাবে সত্য (skip কিছু বদলায় না, আর true সবসময় সত্য)। While rule দেয়:

$\{true\}\ \ \texttt{while}\ true\ \texttt{do skip}\ \ \{true \wedge \neg true\}$

Postcondition true ∧ false = false। Logic-এ false থেকে যেকোনো কিছু follow করে (ex falso quodlibet), আর rule of consequence বলে যদি Q' ⟹ Q হয় তাহলে postcondition Q'-কে যেকোনো দুর্বল Q দিয়ে replace করা যায়। যেহেতু false ⟹ Q (যেকোনো Q-এর জন্য vacuously সত্য), তাই আমরা যেকোনো Q বসাতে পারি।

এটা দুর্বলতা নয় — এটা partial correctness-এর সংজ্ঞার সরাসরি পরিণতি। Partial correctness বলে “যদি থামে, তাহলে Q”। এই loop কখনো থামে না, তাই “যদি থামে” শর্তটা কখনো satisfy হয় না — পুরো statement vacuously সত্য, ঠিক যেমন “যদি 2+2=5, তাহলে চাঁদ পনিরের তৈরি” logically সত্য একটা statement (মিথ্যা premise থেকে)।

এই কারণেই lesson-এর মূল টেক্সটে জোর দেওয়া হয়েছে: partial correctness একা কখনো যথেষ্ট নয় — সবসময় আলাদাভাবে termination (variant function দিয়ে) প্রমাণ করতে হবে। যে কোনো serious verification tool (Dafny, F*) এই দুটোকে একসাথে বাধ্যতামূলক করে, ঠিক এই ফাঁকটা বন্ধ করতে।

সমস্যাটা দুই ভাগে।

প্রথমত, “কখনো দেখিনি” মানে “ঘটেনি না” — মানে “দেখা যায়নি”। Race condition-এর ফলাফল যদি silently ভুল হয় (যেমন counter একটু কম হওয়া, কিন্তু crash না করা), তাহলে bug detect না হয়ে চুপচাপ ভুল ডেটা তৈরি হতে পারে। Production-এ “কখনো দেখিনি” প্রায়ই মানে “কখনো লক্ষ্য করিনি” — একটা payment system-এ ৫০ টাকার discrepancy হয়তো মাসের রিপোর্টে চাপা পড়ে যায়, যতক্ষণ না accumulate হয়ে বড় হয়।

দ্বিতীয়ত, “হাজার বার চলেছে” একটা statistical sample, exhaustive proof না। Production-এর thread scheduler বাস্তবে 20টা possible interleaving-এর মধ্যে সব equally likely চালায় না — কিছু interleaving (যেমন একটা thread সম্পূর্ণ শেষ করে আরেকটা শুরু হওয়া) অনেক বেশি সম্ভাব্য, কারণ context switch ব্যয়বহুল আর scheduler কম করে। তাই bug-উৎপাদনকারী বিরল interleaving হয়তো মিলিয়ন রান-এ একবার ঘটে — production-এ “হাজার বার” এখনো সেই মিলিয়নের ধারেকাছেও না।

Model checking-এর মূল সুবিধা ঠিক এখানেই: এটা “সম্ভাবনার” উপর নির্ভর করে না। এটা প্রতিটা সম্ভাব্য interleaving structurally enumerate করে — rare হোক বা common, exhaustive exploration-এ সবগুলোই সমান গুরুত্ব পায়। এটাই AWS-এর case study-তে দেখা bug-গুলোর pattern: এমন rare timing window যা বছরের production traffic-এও ঘটেনি, কিন্তু TLC কয়েক মিনিটেই খুঁজে বের করেছে।

তিনটাই আলাদা স্তরে, একসাথে ব্যবহারযোগ্য — কোনোটা “সেরা” না, প্রতিটার নিজস্ব জায়গা।

প্রথমে TLA+ দিয়ে protocol-level design। Lock service-এর মূল ঝুঁকি distributed-systems-এর — network partition, node crash, message reorder/loss, concurrent client request। এগুলো precisely এমন জায়গা যেখানে TLA+ সবচেয়ে শক্তিশালী: পুরো protocol-কে state machine হিসেবে লিখে, safety property (একই সময়ে দুইজন lock ধরতে পারবে না) আর liveness property (lock request শেষ পর্যন্ত granted বা denied হবেই — চিরকাল ঝুলে থাকবে না) যাচাই করা। এটা implementation লেখার আগে করা উচিত — design-এর ভুল তখন সস্তায় ধরা পড়ে, কোড লেখার পরে নয়।

তারপর, নির্দিষ্ট critical algorithm-এর জন্য Hoare logic-স্টাইল reasoning। যেমন lock-এর internal state machine-এর একটা sequential অংশ (একটা single node-এর মধ্যে lease renewal logic) — এখানে explicit precondition/postcondition/invariant লেখা (হয়তো Dafny/F*-এর মতো tool দিয়ে, না হলে code comment + assertion হিসেবে) implementation-এর correctness নিশ্চিত করে, protocol-level design ঠিক থাকলেও।

সবশেষে, model checking implementation-এর কাছাকাছি স্তরে। যদি TLA+ spec-এর কাছাকাছি একটা executable model বানানো যায় (বা production code-এর উপর সরাসরি — যেমন Jepsen-এর মতো টুল, যেটা আসল distributed system চালিয়ে network fault inject করে আর observed behavior একটা formal consistency model-এর বিরুদ্ধে checks করে), সেটা implementation আসলেই spec মেনে চলছে কি না তার একটা empirical সেতু — কারণ TLA+ proof শুধু spec সম্পর্কে বলে, code spec সঠিকভাবে implement করেছে কি না তা আলাদা প্রশ্ন (এই ফাঁকটাই Misconception section-এর প্রথম দাবির মূল কথা)।

সংক্ষেপে: TLA+ → design-এর সবচেয়ে ঝুঁকিপূর্ণ (concurrent/distributed) অংশ প্রথমে যাচাই, Hoare-স্টাইল reasoning → sequential algorithm-এর বিস্তারিত সঠিকতা, model checking/testing tool (Jepsen) → code স্পেসিফিকেশন মেনে চলছে কি না তার empirical যাচাই। তিনটা মিলিয়ে trusted base যতটা সম্ভব ছোট করা যায়, একটাও একা সম্পূর্ণ নিশ্চয়তা দেয় না।