The problem that we are going to deal with has to do with the fact that the epistemological and technological milieu of current computer science is rather problematic. There is a dramatic need for dependable information technology. This is the case especially in life critical software or when software is embedded software is mass-produced.
Why is this? Well, the reason is that in both cases a failure in the software can cause either loss of life or loss of money, as the recent mishappenings that have happened in the hardware industry have proved.
Running tests is not enough, because we do not reach that degree of certainty of reliability of our software that we would like. So how can we achieve greater reliability? Is it possible to achieve absolute reliability?
The only viable answer appears to be through rigorous analysis based on formal logic and mathematical models.
It would be nice if we could achieve rigour with the different tools from a formal tool. But with the current technology, the only way we can achieve good rigour is through formal methods.
This is the reason for what I call here plethoric multitude of formal methods in computer science.
There has been really a great increase in the production of formal system for analysing software; so we have specification languages, program logics, some calculi, denotation and operational models, automata, and so on.