This chapter discusses the role of formal methods in software engineering. Formal methods allow software engineers to create specifications using mathematical notation that is more complete, more consistent, and unambiguous. The mathematics used in formal software engineering methods relies heavily on set theory and logic. In many safety critical or mission critical systems, failures can have a high cost. Many safety critical systems can not be completely tested without endangering the lives of the people they are designed to protect. Use of formal methods reduces the number of specification errors dramatically, which means that the customer will encounter fewer errors when the product is deployed.
Using Formal Methods
Define the data invariant, state, and operations for each system function
data invariant - condition true throughout execution of function that contains a collection of data
state - stored data accessed and altered by function
operations - system actions that take place when data are read or written to the state (a precondition and postcondition is associated with each operation)
Specification is represented in some set theoretic type notation from some formal language (e.g., OCL or Z)
Specification correctness can be verified using mathematical proofs (set operations, logic operations, sequences, induction)
Formal Specification Properties
Unambiguous - formal syntax used by formal methods has only one interpretation (unlike natural language statements)
Consistency - ensuring through mathematical proof that initial facts can be mapped (using inference rules) into later statements within the specification
Completeness - difficult to achieve in a large system even using formal methods
Weaknesses of Less Formal Approaches
Contradictions - statements do not agree with one another
Ambiguities - statements have more than one interpretation
Vagueness - specifications in large documents are often not written precisely enough
Incompleteness (e.g., failing to list limitations and error handling required of a function)
Mixed levels of abstraction - occurs when very abstract statements are intermixed randomly with statements written at lower levels of detail)
Necessary Mathematics
Constructive set specification (also known as set builder notation)
Set operations (membership, subset, union, intersection, difference, crossproduct or Cartesian product, powerset)
