Proof
প্রমাণ
গৃহীত সত্য থেকে শুরু করে বৈধ inference rule প্রয়োগ করে লক্ষ্য দাবিতে পৌঁছানোর যুক্তিশৃঙ্খল। Testing দেখায় bug আছে; proof দেখায় নেই।
তিনটা উপাদান: axiom (প্রমাণ ছাড়া গৃহীত), inference rule (বৈধ পদক্ষেপ), আর conclusion।
সবচেয়ে মৌলিক rule দুইটা:
modus ponens: p → q, p ⊢ q
modus tollens: p → q, ¬q ⊢ ¬pআর যে দুইটা বৈধ নয় (মানুষের সবচেয়ে সাধারণ যৌক্তিক ভুল):
p → q, q ⊬ p affirming the consequent
p → q, ¬p ⊬ ¬q denying the antecedent“এই bug হলে log-এ X আসত। Log-এ X আছে। অতএব এই bug।” — অবৈধ।
পাঁচটা কৌশল: direct, [[contrapositive]], contradiction, case analysis, [[counterexample]]। অসীম ক্ষেত্রের জন্য [[induction]]।
Dijkstra-র বাক্যটা এখানে formally বোঝা যায়: “Program testing can be used to show the presence of bugs, but never to show their absence.” — testing একটা existential হাতিয়ার, correctness একটা universal দাবি।
শিল্পক্ষেত্রে: seL4 (verified kernel), CompCert (verified compiler), AWS-এর TLA+ specification, আর Rust-এর borrow checker — সবই machine-checked proof।