Questions: Floyd-Hoare Verification

Question 1

What is a verification condition in the context of Floyd-Hoare verification?

• A. A runtime check inserted into the program to detect violations
• B. A logical formula derived from program annotations that, if valid, guarantees the program meets its specification
• C. A type-checking constraint that ensures the program compiles
• D. A test case that exercises a particular code path

Answer: (B)

Verification conditions are purely logical — they are formulas generated from the program's annotations (preconditions, postconditions, loop invariants) and the program's semantics. If every VC is valid (true in all states), the program is guaranteed correct with respect to its specification. VCs are checked statically by theorem provers or SMT solvers, not at runtime.

Question 2

In Floyd-Hoare verification, the human must supply loop invariants because verification condition generation cannot automatically discover them.

• T. True
• F. False

Answer: True

VC generation is mechanical: given annotations at every loop head and function boundary, the tool computes weakest preconditions backward and checks that each annotation implies what the next one requires. But finding the right loop invariant — an assertion strong enough to prove the postcondition yet weak enough to be preserved by every iteration — is undecidable in general and must be supplied by the programmer or inferred by heuristic tools.

Question 3

A Floyd-Hoare proof of a 50-line function with 3 loops has all its verification conditions discharged by an SMT solver. What has been proven, and what has NOT been proven?

Model answer: What is proven: the function meets its specification (postcondition follows from precondition) assuming the annotations are correct and the language semantics model is faithful. What is NOT proven: termination (unless separately argued with ranking functions), absence of undefined behavior outside the modeled semantics (e.g., stack overflow), or that the specification itself captures the intended behavior.

Floyd-Hoare verification is relative verification — it proves the program correct relative to its specification and its semantic model. If the specification is wrong (says the wrong thing about what the function should do) or the semantic model omits important behavior (like integer overflow in C), the proof does not catch those errors. This is why formal methods practitioners emphasize getting the specification right as the hardest and most valuable part of the process.