Software development is a vital activity in modern American society, and is likely to have increasing significance in the future. Software manages our bank accounts, pays our salaries, controls the aircraft we fly in, regulates power generation and distribution, controls our communications, etc.
High quality software shares the following obvious attributes:
The notion that software components can be reused is a principal motivation of object-oriented programming, and has virtually become a postulate of programming. To reuse a previously written software component (or create a new one), a software engineer must have a precise description of its behavior. This precision is essential as even a minor misconception of the function of a component that is unapparent at the outset may cause serious errors that are difficult and expensive to correct later in the process.
Software development models commonly subdivide the process into phases similar to the following :
Formal methods are intended to systematize and introduce rigor into all the phases of software development. This helps us to avoid overlooking critical issues, provides a standard means to record various assumptions and decisions, and forms a basis for consistency among many related activities. By providing precise and unambiguous description mechanisms, formal methods facilitate the understanding required to coalesce the various phases of software development into a successful endeavor.
The programming language used for software development furnishes precise syntax and semantics for the implementation phase, and this has been true since people began writing programs. But precision in all but this one phase of software development must derive from other sources. The term "formal methods" pertains to a broad collection of formalisms and abstractions intended to support a comparable level of precision for other phases of software development. While this includes issues currently under active development, several methodologies have reached a level of maturity that can be of benefit to practitioners.
There is a discernible tendency to merge discrete mathematics and formal methods for software engineering (e.g., see the books by Denvir, Ince, and Woodcock & Loomes). Many such topics do indeed support software engineering and it is neither possible nor desirable to avoid these topics when pursuing formal methods. But we will not take the approach that applying discrete mathematics to software engineering assures germane formal methods. The overriding concern of software engineering is the creation of high quality software systems. With "formal methods" we pursue melding those things that nurture rigor and precision into this endeavor. While our focus on the activities that precede the actual programming itself does lead to machine independent abstractions often associated with mathematics, much of the material has been developed (or tailored) to suit the context of software creation.
Specific formalisms that will occupy our attention include: