The Domestication of Formal Methods
Almost a full year ago, I concluded that formal methods simply aren’t worth the effort:
While traditional formal methods such as Z might be a little difficult to pick up if your predicate logic is rusty, applying formalisms that are close to the code doesn’t seem that outrageous in perspective. Design-by-contract language extensions such as Spec# for C# or Plural for Java have been stealthily making their way into IDEs for years now without anyone really knowing the wiser, without anyone really thinking about these tools as being formal methods. State machines in UML and even some uses of domain specific languages might be considered formal methods when these tools are used for specification and analysis purposes.
Creating formal methods that are close to the code is one of the best ideas to come out of the formal methods arena in the past 20 years. Just like how adding cherry flavor makes it easier for kids to take icky tasting medicine, putting formal methods in the code makes it more likely that I, as a programmer, will actually use them. Because no matter how good for me something is, if it’s difficult to use or generally unpleasant, it won’t get used.
This is why domesticating formal methods (pdf) is extremely important for formal method adoption.
Wild formal methods can be difficult to work with. No matter what anyone tells you it does take time to get the hang of Z. Formal methods such as Z have limited use when talking with customers and, though a formal specification is an excellent tool for gaining better understanding of functional requirements, the payoff for creating the specification isn’t seen for weeks or months making it difficult to justify their use in Agile development environments.
But is turning what was once a ferocious and unpredictable wolf into an obedient and trusted canine companion safe? In selecting the features for our domesticated formal methods, did we accidentally breed out the most important benefits?
Anthony Hall outlined seven myths of formal methods (pdf), ideas about formal methods erroneously taken as truth.
Myth 1: Formal methods can guarantee that software is prefect
Myth 2: Formal methods are all about program proving.
Myth 3: Formal methods are only useful for safety-critical systems.
Myth 4: Formal methods require highly trained mathematicians.
Myth 5: Formal methods increase the cost of development.
Myth 6: Formal methods are unacceptable to users.
Myth 7: Format methods are not used on real, large-scales software.
Any formal method worth using should not uphold any of Hall’s seven myths, but domesticated formal methods have the additional burden of usability. Just like we expect certain behavior from our four-legged friends, I don’t think it’s too much to ask that a domesticated formal method be friendly and obedient. Any method which bites the master’s hand obviously can’t be trusted. Crashing, making it easy to make mistakes, poor affordances, difficult to read output, impossible to maintain specifications – these are all reasons for not trusting a domesticated formal method.
I think informal formal methods are great. When done well, it doesn’t even feel like I’m using a formal method and I get many of the same benefits a wild formal method would give me – clarity, understanding, and maybe even a little automated verification depending on the language and method. Domain specific languages and state charts are great for working with end users and clients. It’s even plausible to skip other testing or verification measures such as unit testing or inspection.
And the best part is that since many domesticated formal methods are close to the code, I’ve already got the necessary training on how to use the methods because I already know how to program. Domesticated formal methods are a win-win for programmers who want to do more engineering and another practical tool for your silver toolbox.
For almost every project in the world, I think formal methods should be generally avoided. Given the option of spending money and time on mathematicians or extremely smart coders I would chose the latter. With smart coders, code inspection is a fun and effective defect filtering option. And let’s face it. Why would you have your amazing coders do something other than write amazing code?But what if formal methods didn’t have to be so...formal?
While traditional formal methods such as Z might be a little difficult to pick up if your predicate logic is rusty, applying formalisms that are close to the code doesn’t seem that outrageous in perspective. Design-by-contract language extensions such as Spec# for C# or Plural for Java have been stealthily making their way into IDEs for years now without anyone really knowing the wiser, without anyone really thinking about these tools as being formal methods. State machines in UML and even some uses of domain specific languages might be considered formal methods when these tools are used for specification and analysis purposes.
Creating formal methods that are close to the code is one of the best ideas to come out of the formal methods arena in the past 20 years. Just like how adding cherry flavor makes it easier for kids to take icky tasting medicine, putting formal methods in the code makes it more likely that I, as a programmer, will actually use them. Because no matter how good for me something is, if it’s difficult to use or generally unpleasant, it won’t get used.
This is why domesticating formal methods (pdf) is extremely important for formal method adoption.
Wild formal methods can be difficult to work with. No matter what anyone tells you it does take time to get the hang of Z. Formal methods such as Z have limited use when talking with customers and, though a formal specification is an excellent tool for gaining better understanding of functional requirements, the payoff for creating the specification isn’t seen for weeks or months making it difficult to justify their use in Agile development environments.
But is turning what was once a ferocious and unpredictable wolf into an obedient and trusted canine companion safe? In selecting the features for our domesticated formal methods, did we accidentally breed out the most important benefits?
Anthony Hall outlined seven myths of formal methods (pdf), ideas about formal methods erroneously taken as truth.
Myth 1: Formal methods can guarantee that software is prefect
Myth 2: Formal methods are all about program proving.
Myth 3: Formal methods are only useful for safety-critical systems.
Myth 4: Formal methods require highly trained mathematicians.
Myth 5: Formal methods increase the cost of development.
Myth 6: Formal methods are unacceptable to users.
Myth 7: Format methods are not used on real, large-scales software.
Any formal method worth using should not uphold any of Hall’s seven myths, but domesticated formal methods have the additional burden of usability. Just like we expect certain behavior from our four-legged friends, I don’t think it’s too much to ask that a domesticated formal method be friendly and obedient. Any method which bites the master’s hand obviously can’t be trusted. Crashing, making it easy to make mistakes, poor affordances, difficult to read output, impossible to maintain specifications – these are all reasons for not trusting a domesticated formal method.
I think informal formal methods are great. When done well, it doesn’t even feel like I’m using a formal method and I get many of the same benefits a wild formal method would give me – clarity, understanding, and maybe even a little automated verification depending on the language and method. Domain specific languages and state charts are great for working with end users and clients. It’s even plausible to skip other testing or verification measures such as unit testing or inspection.
And the best part is that since many domesticated formal methods are close to the code, I’ve already got the necessary training on how to use the methods because I already know how to program. Domesticated formal methods are a win-win for programmers who want to do more engineering and another practical tool for your silver toolbox.
Comments
Post a Comment