Formal Specifications: Beyond Instructions, Defining Software Behaviors
2025-07-28
This post delves into the distinction between formal specifications and traditional programs. While programs are lists of instructions, formal specifications are sets of behaviors. Using a counter example, the author illustrates how specifications define all correct behaviors and leverage set theory, employing generators (Init and Next) to describe infinite sets of behaviors. This contrasts with the concept of nondeterminism in programming; in formal specifications, nondeterminism refers to multiple ways a behavior can be extended, while in programs, it refers to uncertain code paths. The article emphasizes understanding formal specifications as sets of behaviors, crucial for debugging and interpreting model checker errors.