Beyond Hoare Logic

Euclidean Algorithm Specification

• Method to find gcd(x: nat, y: nat)

  • Requires x != 0 && y != 0

  • Ensures n == gcd(x,y)

  • Uses gcd function for precise postcondition

Function as Specification

• Function gcd(x: nat, y: nat) defined recursively
  • Returns x if x == y
  • If x > y, calls gcd(x-y, y)
  • If y > x, calls gcd(x, y-x)
  • Provides executable specification
  • Must ensure termination of recursion

Function Termination Condition

• Requires well-founded recursion
  • Parameters must strictly decrease
  • Ensures x+y decreases with each call
  • Dafny checks termination automatically.

Specification Benefits

• Improves readability of code
  • Enables recursive specifications
  • Provides executable reference implementation
  • Must include termination proof for recursion.

Verification History Timeline

• Turing (1949): Program correctness
  • Floyd (1967): Flowchart reasoning
  • Hoare (1969): Hoare logic
  • Dijkstra (1976): Weakest precondition
  • Back (1980): Stepwise refinement
  • Jones (1981): Rely/guarantee
  • Abrial (1996): B Method
  • Reynolds (2002): Separation logic
  • McIver/Morgan (2005): Probabilistic reasoning
  • Platzer (2018): Differential dynamic logic
  • Daggitt et al. (2022): Neural network verification.

Stepwise Refinement

• Method for constructing correct-by-construction programs
  • Involves a series of refinement steps
  • Each step preserves correctness
  • Semantics described by weakest preconditions.

Rely/Guarantee Reasoning

• Extension of Hoare logic for concurrent programs
  • Rely condition: Assumptions about other processes
  • Guarantee condition: Commitments to other processes
  • Compositional proof technique for concurrency.

B Method

• Industrial verification method used in Paris Metro Line 14
  • Influenced by Dijkstra's weakest precondition
  • Event-B extends to system development
  • Widely applied in railway domain.

Separation Logic

• Extension of Hoare logic for low-level programs
  • Compositional reasoning about heaps
  • Basis for Facebook Infer static analysis tool
  • Handles shared mutable data structures.

Probabilistic Reasoning

• Introduced probabilistic predicate transformers
  • Focuses on programs with stochastic behaviors
  • Provides quantitative reasoning
  • Distinguishes between probabilistic and non-deterministic programs.

Differential Dynamic Logic

• Framework for hybrid systems
  • Based on Hoare logic
  • Includes compositional reasoning with differential equations
  • Verified applications in autonomous driving and aviation.

Vehicle Language

• Domain-specific language for neural network verification
  • Interfaces with interactive theorem provers
  • Enhances maintainability and scalability
  • Embeds logical specifications into neural networks.

Turing Award Winners in Verification

• Edsger Dijkstra (1972): Program correctness
  • Robert Floyd (1978): Flowchart reasoning
  • Tony Hoare (1980): Hoare logic foundations.

Alan Turing's Contribution

• Proposed method for verifying program correctness
  • Suggested making definite assertions
  • Aims to establish overall program correctness.

Floyd's Flowcharts

• Developed a diagrammatic notation
  • Used for reasoning about programs rigorously
  • Extended meanings to program assertions
  • Influenced Hoare logic's development.

Hoare Logic Evolution

• Also termed Floyd-Hoare logic
  • Axiomatic system for program reasoning
  • Focuses on pre/postconditions
  • Foundational for modern verification.

Dijkstra's Weakest Precondition

• Strategy for valid deductions in Hoare logic
  • wp(S, Q): weakest precondition for establishing Q
  • Enables automated verification of programs.