| Software is built on abstractions. Pick the right ones, and programming
will flow naturally from design; modules will have small and simple interfaces;
and new functionality will more likely fit in without extensive
reorganization. Pick the wrong ones, and programming will be a series
of nasty surprises: interfaces will become baroque and clumsy as they
are forced to accommodate unanticipated interactions, and even the
simplest of changes will be hard to make. No amount of refactoring,
bar starting again from scratch, can rescue a system built on flawed
concepts.
This book presents a new approach. It takes from formal specification
the idea of a precise and expressive notation based on a tiny core of
simple and robust concepts, but it replaces conventional analysis based
on theorem proving with a fully automatic analysis that gives immediate
feedback. Unlike theorem proving, this analysis is not “complete”:
it examines only a finite space of cases. But because of recent advances
in constraint-solving technology, the space of cases examined is usually
huge—billions of cases or more—and it therefore offers a degree of coverage
unattainable in testing.
Moreover, unlike testing, this analysis requires no test cases. The user
instead provides a property to be checked, which can usually be expressed
as succinctly as a single test case. A kind of exploration therefore
becomes possible that combines the incrementality and immediacy
of extreme programming with the depth and clarity of formal specification. |
