Hoare Logic

{P} C {Q} — P precondition, C প্রোগ্রাম/স্টেটমেন্ট, Q postcondition। পাঁচটা মূল inference rule: assignment ({Q[E/x]} x:=E {Q} — পেছন থেকে সামনে), sequence, if, while (loop invariant দিয়ে), আর rule of consequence (precondition শক্তিশালী/postcondition দুর্বল করা)।

Partial correctness বলে “যদি থামে, তাহলে Q সত্য”; total correctness-এ termination-ও (variant function দিয়ে) প্রমাণ করতে হয়। Loop invariant-ভিত্তিক প্রমাণ আসলে mathematics/induction-এরই একটা প্রয়োগ — invariant maintenance step inductive step-এর সমতুল্য।

আধুনিক static verifier (Dafny, Frama-C) আর security module-এর memory-safety যাচাই টুলগুলোর ভিত্তি এই একই triple-notation।