Formal Models: I Hate You, I Love You
My view on formal methods is somewhat... nuanced. In spite of this I'll go ahead and start with a ridiculously strong and outrageous assertion that I can use as a toe hold for further discussion: Formal specifications do not have a place in agile software development. Don't get me wrong. As a software engineer I like the idea of formal specifications very much. They are precise. They are unambiguous. They are... engineering-y. But as a post-modernist software engineer I also think formal specifications are kind of a dumb idea. They are tedious. They are cryptic. They are... anti-human.
For decades software engineers seem to have put formal specifications on a pedestal as if they were the Michelangelo's David of requirements. But while Michelangelo's sculpture of David manages to perfectly capture the essence of humanity in marble, even the most elegant formal specifications fail to fully capture the perfect essence of desired functional behavior of a software system. The fatal flaw of formal specification comes from removing the human element and assuming that cold mathematical precision is an adequate model for communicating and comprehending human desires. (Yes, I am creating a straw man, but please allow me to beat him up just a little more before providing a counterpoint.)
A common example formalists use to demonstrate the strengths of formal specification (and weaknesses of plain old English prose) comes from the alleged ambiguity and confusion created by various warning signs posted by escalators throughout the UK. "Dogs must be carried," the signs read. "What if I don't have a dog? Can I still use this escalator?" the formalists rhetorically ask, I always imagine with a smug grin.
This argument of course is completely absurd. Contextually, no confusion exists. If you have a dog, then carry it up the escalator. The formalist may ask next, "What if I only own a cat?" Ugh. Formal models may be more precise but this does not mean they are necessarily more correct or more complete. Whether using natural language or a formal model, the question of cats (or goats or fish or pythons) is still a good one. Chances are good you may ride the escalator if you are not carrying a dog. Also, you probably should carry your cat too. (Another great example for those interested: the TSA wants everyone to pack gel-filled brassieres.)
The common fallacy is that formal specification seems to encourage the incorrect assumption that more formal a model the more correct it is. This confusion is likely created by confounding precision with correctness. The goal is to create the most correct and precise model as possible so that you have an irrefutable representation of the system, a representation that has no room for argument or confusion. This is certainly a positive intention, albeit slightly misguided. From an Agile perspective the goal should not be to create something that cannot be refuted but rather to facilitate effective communication. In a world where collaboration is strongly preferred over negotiation perfection is the enemy that will drive you and your customer apart. There is no thin red line in a healthy customer-team relationship.
This is not to say that ambiguous requirements are desirable. The confusion is in the message sent by the type of specification that you use. The mathematical obfuscation and high-brow attitude of formal modeling sends all the wrong signals and can even make it more difficult to create a correct model. For the average customer, offering up formal specifications as an irrefutable, unambiguous, no room for error model is the equivalent of saying, "Hey client, I don't care if you can't understand this and your needs are not important to me. I really just want to cover my ass here so I can throw your desires over the wall for construction." Precision, correctness, completeness, and a lack of ambiguity are important traits for any specification, but so too is effective communication and a certain degree of flexibility to forge a new path as new information becomes available.
Formal specifications seem to be born from a fixed mindset, a good match for folks who cannot (or simply refuse to) operate without exacting precision and firm, non-negotiable interpretations of "right" and "wrong." Unfortunately, "right" and "wrong" are very relative notions on most software projects and "better" or "worse" is the currency in which we deal. Understanding whether something is better, or even just good enough, is often relative and can only be fully understood once you have seen a solution if only a partially working one.
And yet...
And yet, I am still an engineer at heart and do not want to throw the formal baby out with the bathwater. Formal specification might still be useful in an agile context as long as the methods complement agile values. Behavior Driven Development, design-by-contract with predicates and post-conditions, automated functional testing – these are all models in the spirit of formal specification without the high-brow, non-negotiable attitude. What's more methods like these aim to enhance communication between customer and team, and even within a team, rather than obfuscate it. A good old fashioned state machine sometimes really is the best medicine, but in my experience it is a tool that can only be used effectively with the right set of stakeholders.
Communication is something everyone can agree is a good thing, at least in theory. Even the most ardent Z supporters will tell you that one of most valuable aspects of a Z specification is in the prose that accompanies the model. Meanwhile, those same Z supporters will breathlessly defend formal methods, even though they just admitted that the informal part is one of the most valuable pieces, that the formal model really should not exist without the explanatory prose. The model is really just a tool, a means to an end for achieving clarity in thinking.
What I am proposing is not to abandon formal specifications. Formal modeling is an awesome tool - when used with the right frame of mind. Formal models that embrace agile values and promote humanist qualities are the ones you should be using. Why not make that model, or the prose surrounding it, executable? Why not rely on contextual or cultural cues to enhance meaning? Why not use comprehensible prose, diagrams, sketches, prototypes, tests, and working software in combination to reduce ambiguity, enhance precision, and improve correctness while enabling true collaboration?
Pragmatic, human-centered formal methods have an important place in Agile software development and should be embraced wholeheartedly.
For decades software engineers seem to have put formal specifications on a pedestal as if they were the Michelangelo's David of requirements. But while Michelangelo's sculpture of David manages to perfectly capture the essence of humanity in marble, even the most elegant formal specifications fail to fully capture the perfect essence of desired functional behavior of a software system. The fatal flaw of formal specification comes from removing the human element and assuming that cold mathematical precision is an adequate model for communicating and comprehending human desires. (Yes, I am creating a straw man, but please allow me to beat him up just a little more before providing a counterpoint.)
A common example formalists use to demonstrate the strengths of formal specification (and weaknesses of plain old English prose) comes from the alleged ambiguity and confusion created by various warning signs posted by escalators throughout the UK. "Dogs must be carried," the signs read. "What if I don't have a dog? Can I still use this escalator?" the formalists rhetorically ask, I always imagine with a smug grin.
 |
| The more important question: What happened to that dog's butt? |
This argument of course is completely absurd. Contextually, no confusion exists. If you have a dog, then carry it up the escalator. The formalist may ask next, "What if I only own a cat?" Ugh. Formal models may be more precise but this does not mean they are necessarily more correct or more complete. Whether using natural language or a formal model, the question of cats (or goats or fish or pythons) is still a good one. Chances are good you may ride the escalator if you are not carrying a dog. Also, you probably should carry your cat too. (Another great example for those interested: the TSA wants everyone to pack gel-filled brassieres.)
The common fallacy is that formal specification seems to encourage the incorrect assumption that more formal a model the more correct it is. This confusion is likely created by confounding precision with correctness. The goal is to create the most correct and precise model as possible so that you have an irrefutable representation of the system, a representation that has no room for argument or confusion. This is certainly a positive intention, albeit slightly misguided. From an Agile perspective the goal should not be to create something that cannot be refuted but rather to facilitate effective communication. In a world where collaboration is strongly preferred over negotiation perfection is the enemy that will drive you and your customer apart. There is no thin red line in a healthy customer-team relationship.
This is not to say that ambiguous requirements are desirable. The confusion is in the message sent by the type of specification that you use. The mathematical obfuscation and high-brow attitude of formal modeling sends all the wrong signals and can even make it more difficult to create a correct model. For the average customer, offering up formal specifications as an irrefutable, unambiguous, no room for error model is the equivalent of saying, "Hey client, I don't care if you can't understand this and your needs are not important to me. I really just want to cover my ass here so I can throw your desires over the wall for construction." Precision, correctness, completeness, and a lack of ambiguity are important traits for any specification, but so too is effective communication and a certain degree of flexibility to forge a new path as new information becomes available.
Formal specifications seem to be born from a fixed mindset, a good match for folks who cannot (or simply refuse to) operate without exacting precision and firm, non-negotiable interpretations of "right" and "wrong." Unfortunately, "right" and "wrong" are very relative notions on most software projects and "better" or "worse" is the currency in which we deal. Understanding whether something is better, or even just good enough, is often relative and can only be fully understood once you have seen a solution if only a partially working one.
And yet...
And yet, I am still an engineer at heart and do not want to throw the formal baby out with the bathwater. Formal specification might still be useful in an agile context as long as the methods complement agile values. Behavior Driven Development, design-by-contract with predicates and post-conditions, automated functional testing – these are all models in the spirit of formal specification without the high-brow, non-negotiable attitude. What's more methods like these aim to enhance communication between customer and team, and even within a team, rather than obfuscate it. A good old fashioned state machine sometimes really is the best medicine, but in my experience it is a tool that can only be used effectively with the right set of stakeholders.
Communication is something everyone can agree is a good thing, at least in theory. Even the most ardent Z supporters will tell you that one of most valuable aspects of a Z specification is in the prose that accompanies the model. Meanwhile, those same Z supporters will breathlessly defend formal methods, even though they just admitted that the informal part is one of the most valuable pieces, that the formal model really should not exist without the explanatory prose. The model is really just a tool, a means to an end for achieving clarity in thinking.
What I am proposing is not to abandon formal specifications. Formal modeling is an awesome tool - when used with the right frame of mind. Formal models that embrace agile values and promote humanist qualities are the ones you should be using. Why not make that model, or the prose surrounding it, executable? Why not rely on contextual or cultural cues to enhance meaning? Why not use comprehensible prose, diagrams, sketches, prototypes, tests, and working software in combination to reduce ambiguity, enhance precision, and improve correctness while enabling true collaboration?
Pragmatic, human-centered formal methods have an important place in Agile software development and should be embraced wholeheartedly.
Comments
Post a Comment