Submitted by The Alloy Analyzer is a tool developed by MIT for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. Alloy can be used to detect conceptual mistakes in the model before the coding starts. Scientific American has published an article about it.
Seems like you need to write code twice. Translating alloy code to real program code can introduce errors, too.
Better compilers and debuggers maybe will do more to make software more reliable.
Seems like you need to write code twice.
You’re only formalizing the design in Alloy not creating an implementation, so there’s not so much code duplication.
Think of it as simulation software, where for example you might create a simulation of a city to test how public transport, utilities, etc operate. Only once your simulation performs adequately do you build the actual city with bricks and mortar. Obviously, it’s much cheaper to discover problems in your design before you’ve built half the city.
Similarly when modeling a software design in Alloy, you’re not creating the final application (no GUI, no industrial control code, etc). Instead you’re creating a simulation of all the objects that will ultimately exist and codifying how they will interact with each other.
Translating alloy code to real program code can introduce errors, too.
Of course that’s true but they should be less severe than errors created by a flawed ad hoc design.
Better compilers and debuggers maybe will do more to make software more reliable.
Better compilers and debuggers don’t help much when your basic design is based on a flawed abstraction.