As a software engineer, one of my fears is discovering a showstopping bug right before a big release. The kind of bug that requires going back to the drawing board with very little time to design and implement a fix. If I could find a tool that makes it easier to find serious bugs in the early stages of a project, that would justify a lot of time spent learning it.
Alloy
On a recent project at work, I had a hunch about an edge case that could affect a significant number of users, but thinking through all of the possibilities was starting to get overwhelming. In situations like this, writing things down usually helps to clarify my thoughts, but I just couldn’t find the right words to express exactly how a user might end up in this weird state.
In an effort to make things a bit more rigorous, I started trying to model the problem with the Alloy specification language. I had been curious about formal methods (and model checkers in particular) for a while, and this seemed like a good place to start.
I was able to create a very simple model in a few hours, and verified that the edge case was an actual bug.
Confirming suspicions
In this situation, I already had the edge case in mind, and it influenced the Alloy model that I wrote. If I were modeling the system from scratch, I wouldn’t have made the same decisions, and probably never would have found the bug.
Using Alloy didn’t result in the discovery of any new bugs, but it was useful for confirming my suspicions about a bug I was vaguely aware of. It provided some peace of mind during a stressful point in the project.
How does a tool like Alloy fit into an Agile development process?
I haven’t recommended Alloy to the rest of my team yet. While I suspect that my coworkers would also find it useful, I don’t think I’m at the point where I can make a compelling argument in favor of adopting it.
Keeping an Alloy model in sync with a codebase over a long period of time would require a lot of discipline. It’s probably not feasible for most large-scale software projects, unless it’s only used for small components that don’t change very often.
I wonder if formal methods and Agile are fundamentally incompatible. I’m sure there’s a way to shoehorn a tool like Alloy into an Agile development process, but it doesn’t seem like a natural fit.
Next steps
I plan to continue using Alloy as a tool for myself, whenever a problem starts to become a little overwhelming. There’s a fun, exploratory aspect to Alloy that I haven’t quite experienced yet. As I get more comfortable with Alloy and other formal methods, I’m hopeful that modeling a system can result in unexpected discoveries.