🗄️ OLD — Formal Specification and Proofs of Correctness (consolidated)

CSS Computer Science (Optional) — Paper-I, Section-B, Topic V. Covers two distinct syllabus items: Formal Specification and Introduction to Proofs of Correctness, which the official syllabus labels with the parenthetical "(LNO)." Neither has appeared in the papers reviewed for this project so far (2019–2026) — treat that as "unconfirmed," not "won't appear": both are still official, examinable syllabus lines, and are the kind of item FPSC uses to catch aspirants who only prepare repeated questions.

Formal Specification

Writing a system's requirements in mathematically precise notation instead of natural language, so the specification itself can be checked for consistency and completeness before a single line of code is written.

• Motivation: natural-language specs are inherently ambiguous ("the system shall respond quickly" — how quickly?). Safety-critical or high-assurance systems (avionics, medical devices, financial settlement) can't tolerate that ambiguity.
• Trade-off: rigour and precision, at the cost of the extra time and mathematical expertise required to write and read the specification.
• Named notation: Z notation — built on set theory and predicate logic, used to describe system state and operations precisely. (VDM is another example worth being able to name.)

Introduction to Proofs of Correctness (the syllabus's "LNO")

The FPSC syllabus lists this item with the parenthetical exactly as "(LNO)" without expanding it in the source document — treat the underlying concept, not the acronym, as the exam-relevant content. This is Hoare-logic-style reasoning: proving mathematically that a program satisfies its specification for all valid inputs, rather than testing it on a finite sample of inputs.

• Precondition: a condition that must be true before a piece of code executes (e.g. "the input array is non-empty").
• Postcondition: a condition that must be true after the code executes (e.g. "the array is sorted in ascending order").
• Loop invariant: a condition that remains true on every single pass through a loop — the standard tool for proving a loop actually achieves its postcondition, rather than merely appearing to on the test cases you happened to try.
• Hoare triple: written {P} S {Q} — "if precondition P holds, and statement S executes, then postcondition Q will hold afterward."
• Why it matters relative to testing: as Dijkstra's well-known observation goes, testing can show the presence of bugs, but formal proof aims to guarantee their absence — for the specific property being proven, across every input, not just the ones tested.

⚠️

This page pairs directly with Formal Specification above — both are "formal methods," and a combined question on why rigorous, mathematics-based approaches matter for critical systems is a plausible way FPSC could test either topic.

MCQ Trap

• "Guarantees no bugs for every input" describes a proof of correctness; "found no bugs in the cases we tried" describes testing — these are not the same claim, and an exam question may hinge on exactly this gap.