The importance of abstraction
Software is built on abstractions.
No amount of refactoring can rescue a system built on flawed concepts.
First, you design the abstractions, then you develop its embodiments in code. Unfortunately, this approach rarely works.
The problem is wishful thinking. When you implement the abstractions, they turn out to be incoherent and inconsistent.
There are two solutions to the solution of wishful thinking: “extreme programming” and “formal specification”.
Formal specification has two obstacles: succinct mathematical notations hard to understand and the lack of tools. Theorem provers demand effort more than is feasible for most software projects.
Alloy 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.
Unlike testing, this analysis requires no test cases. The users instead provides a property to be checked.
Except from Daniel Jackson’s Software Abstraction book Chapter 1.
You can see an example from this blog post.
