
113
6Chapter
Formal Methods
Motivation
Systems have tremendous sensitivity to errors in a requirements specification—even
a misplaced comma can have severe consequences. In code implementation, it is
obvious that misplacing even a single character can make a great deal of difference.
In fact, the accidental substitution of a period for a comma in a single Fortran
statement resulted in the loss of the Mariner 1, the first American probe to Venus
in 1962. But how can such a serious problem exist when misplacing a character in
a requirements specification? Let’s see how that might be so.
e title of Lynne Truss’s 2004 book on punctuation, Eats Shoots ...