Introduction to Proofs of Correctness (LNO)

CSS CS Optional — Paper-I, Section-B, Topic V. Syllabus lists this as "(LNO)" without expanding it — focus on the concept. ⚠️ Not confirmed in past papers reviewed (2019–2026) yet — still fully examinable.

🔑 Formal Specification (background)

• Requirements written in mathematically precise notation, not natural language.
• Motivation: natural language is ambiguous ("respond quickly" — how quickly?). Critical for safety-critical systems (avionics, medical, finance).
• Named notation: Z notation (set theory + predicate logic). Also: VDM.

📌 Proofs of Correctness — Hoare-Logic Reasoning

• Precondition — must be true before code runs.
• Postcondition — must be true after code runs.
• Loop invariant — true on every pass through a loop.
• Hoare triple: {P} S {Q} — if P holds and S executes, then Q holds after.
• Testing vs Proof: testing shows presence of bugs; proof aims to guarantee their absence (Dijkstra).

⚠️ MCQ Trap

• "Guarantees no bugs for every input" = proof of correctness.
• "Found no bugs in cases tried" = testing. Not the same claim.