Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

If you have been trained in the use of formal methods (FM) for programming:

  • How useful have you found it?
  • What did your FM training involve (e.g. a course, a book)?
  • What FM tools do you use?
  • What advantages in speed/quality has it given you compared to not using FM?
  • What kind of software do you create with FM?
  • And if you don't directly use FM now, was it at least worth learning??

I'm curious to hear as many experiences/opinions on FM as can be found in this community; I'm starting to read up on it and want to know more.

Background

Programming and software development/engineering are some of the newest human skills/professions on Earth, so not surprisingly, the field is immature — that shows in our field's main output, as code that is typically late and error-prone. Industry immaturity is also shown by the wide margin (at least 10:1) in productivity between average and top coders. Such dismal facts are well covered in the literature, and introduced by books like Steve McConnell's Code Complete.

The use of formal methods (FM) has been proposed by major figures in software/CS (e.g. the late E. Dijkstra) to address (one of) the root causes of errors: the lack of mathematical rigour in programming. Dijkstra, for instance, advocated for students developing a program and its proof together.

FM seems to be much more prevalent in CS curricula in Europe compared to the US. But in the past few years, new "lightweight" FM approaches and tools like Alloy have attracted some attention. Still, FM is far from common usage in industry, and I'm hoping for some feedback here on why.

Update

As of now (10/14/2010), of the 6 answers below, no one has clearly argued for the usage of FM in "real world" work. I'm really curious if someone can and will; or perhaps FM really does illustrate the divide between academia (FM is the future!) and industry (FM is mostly useless).

share|improve this question
    
Regarding your update, maybe no one has argued for the usage of FM in "real world" work because there are very few use cases for them in real world work –  Richard Nov 3 '11 at 12:42
add comment

6 Answers

Absolutely useless for anything nontrivial.

I had a course called, aptly, "Formal Methods" that focused on Alloy- I can't possibly see using that anywhere. Had another class that focused on concurrency modeling with LTSA- equally useless.

The problem is that most bugs and problems in software (at least in my experience) arise from complexity that occurs below the level of abstraction of those tools.

share|improve this answer
    
Thanks for sharing; Would you say the training in FM was at least helpful to your later work, e.g. helped you think more clearly? Or not? –  limist Oct 7 '10 at 23:34
    
@limist: I really don't think so. I mean, I kinda liked Alloy, but I don't think it was useful even just to expanding how I think. –  Fishtoaster Oct 8 '10 at 4:08
2  
This is exactly the answer I would have given. The most totally redundant class I took at university and not something I have ever looked back on and been glad I learned it. I think the root of the problem is that the Formal Specification must be more complex than the code in order to model it correctly, so for any remotely complex code it's a massively arduous task creating a formal model of it, to the point that I can't imagine anyone outside hardware design or similarly irrevocable work wanting or being able to do it. –  glenatron Oct 14 '10 at 21:39
    
That's disappointing. I was imagining it might be useful for testing that you had a reasonably complete model; while the actual bugs would most often be below the model (screwing up the mutexes or whatever), I assumed it would be useful to use Alloy to find flaws in the model itself. (Intuitively it seems less likely to be useful to try to use a proof assistant; I'd expect counterexamples to be more useful, and that seems more in the domain of things like Alloy (though ideally I guess it would be good to be able to approach both in the same system).) –  Bruce Stephens Dec 20 '12 at 16:04
add comment

I have a background in CSP (Communicating Sequential Processes). Not to toot my own horn but I wrote my Master's thesis on Timed CSP, particularly "compiling" specifications written in formal methods into executable C++. I can say I have some experience with formal methods. Once I completed my degree and got a job in the industry, I have not been using formal methods at all. Formal methods is still too theoretical to be applied in the industry. Formal methods have found some practical application in the area of embedded systems. For example, NASA uses formal methods in their projects. I would speculate that formal methods are very far from being widely adopted in the industry. It simply does not make sense to write software specifications in formal methods and then "human interpret" them to your framework of choice. Plain English and diagrams work better for that, while unit and integration tests have been doing a pretty good job of "verifying" the correctness of code. I think formal methods will remain in the world of academia for some time.

share|improve this answer
    
Thanks for sharing, I'll ask a follow-up repeated often on this Q: Would you say the training in FM was at least helpful to your later work, e.g. helped you think more clearly? Or not? –  limist Oct 7 '10 at 23:35
    
Congrats on your masters! –  Chris Oct 8 '10 at 0:13
    
@limist: I would say it was a very good theoretical experience, but I found very little practical application in the industry. –  ysolik Oct 8 '10 at 3:24
add comment

I've read a few books about formal methods, and applied some. My immediate reaction was, "Gee, these books tell me how to be a good programmer, as long as I'm a perfect mathematician." Another weakness is that you can only prove equivalence with another formal description. Writing up a formal specification for a program is tantamount to writing a program in a higher-level language, and there's no way you can avoid introducing bugs in a reasonably large spec.

I've never made formal methods work on a large scale. They can be useful in getting something small and tricky correct, and in convincing me that they're correct. In that way, I can work with slightly larger building blocks and sometimes get a little more done.

One thing I did pick up that is more generally useful is the concept of an invariant, a statement about a program and its state that is always true. Anything you can reason from is good.

As alluded to above, I'm not a perfect mathematician, and so my proofs sometimes contain errors. However, in my experience these tend to be big dumb mistakes that are easy to catch and fix.

share|improve this answer
add comment

I took a graduate course in formal program analysis, where we focused on operational semantics. I did my final paper on the seL4 effort, reviewing the formal methods they used. My primary take-away in terms of practicality was that it's of marginal value. Not only do you have to write the program, you have to write the proof. Wow. Two sources of bugs. Not just one. Further, there was an enormous amount of restrictions placed on the actual code. It's very hard to formally describe a physical computer, including I/O.

share|improve this answer
    
I once saw a stab at describing tape-style I/O. The author had no solutions for formally describing random access files, and contented himself with badmouthing them. –  David Thornley Oct 8 '10 at 17:43
    
@David: Those random-access files. Bad news. You don't want to use them. =) –  Paul Nathan Oct 8 '10 at 20:19
add comment

I used to work in a department at ICL, before they were bought up by Fujitsu. They had some large government-type contracts that required proof that the software worked as advertised, so they built a machine that would take the formal specification written in Z and validate the code as it ran, with a big green or red light for pass/fail.

It was an amazing thing, but, as the esteemed @FishToaster points out, it was useless for anything non-trivial.

share|improve this answer
add comment

State diagrams and Petri nets are useful for modelling and analyzing protocols and realtime systems. First they help design a solution. Second they help find test cases for exciting software in very specific situations.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.