Software Verification and Axiomatic Semantics

Introduction

• Software verification is often confused with testing.
• Verification involves proving that a program is free of bugs, unlike testing, which finds bugs.
• Testing guru James Whittaker criticized formal methods in a joke, illustrating the lack of interest in loop invariants among practitioners.
• The lecture uses a quiz format to elucidate the necessity of formal verification techniques.

Program Attempts

Attempt #1

• Goal: Implement binary search to find an element in a sorted array.
• Problem: Program does not account for all cases, leading to failure.
• Key issue: Requires single counterexample to disprove correctness.

Attempt #2

• Attempt to improve by ensuring i and j always change.
• Still incorrect; fails for trivial cases (e.g., array of size 1).

Attempt #3

• Modified approach again.
• Includes integer division for midpoint calculation.
• Still incorrect due to out-of-bounds access.

Attempt #4

• Adjustments made to initialize i and j to prevent out-of-bounds.
• Still incorrect for certain edge cases.

Attempt #5 and #6

• #5 is close but still incorrect due to integer overflow.
• #6 adjusts midpoint calculation to prevent overflow using i + (j - i) // 2.
• Version #6 is correct but requires proof.

Program Prover (AutoProof)

• AutoProof is a tool for verifying program correctness.
• Loop invariant is a crucial concept for verification:
  • Must hold after initialization.
  • Must be preserved by loop body.
  • Combined with exit condition, helps prove correctness.
• AutoProof uses formal methods to verify invariants without executing the program.

Understanding Proof Techniques

• Loop Invariant: A condition that remains true throughout the execution of the loop.
• Loop Variant: An integer quantity that decreases with each loop iteration, guaranteeing termination.
• Example invariant properties:
  • Indices are within range.
  • Result is valid if non-zero.
  • Specific array intervals do not contain the target.
  • Result is accurate when exit condition is met.

Lessons Learned

• Binary Search: Used as an example to demonstrate verification challenges.
• Importance of understanding and applying invariants to ensure program correctness.
• Historical context: Early verification work was manual; now automated tools exist.
• Invariants and variants are essential in developing reliable algorithms.
• The evolution of tools like AutoProof demonstrates the significant progress in software verification over decades.

Conclusion

• Writing correct programs requires understanding invariants deeply.
• Verification tools, while advanced, rely on foundational concepts established decades ago.
• The iterative approach in programming is essential for verifying correctness across all cases.