🚀 go-pugleaf

In article <1992Aug12.150936.16184@porthos.cc.bellcore.com>, haim@dancer.uucp (24103-kilov) writes:
|> 
|> "Besides, the crucial thing about Formal Methods is "What tool support is
|> available" - and be suspicious of "tools" as well!! There are few real good
|> ones."
|> 
|> Absolutely not! A formal method is used to understand what you are talking
|> about, i.e., to specify the "system" better. If, as a result of its use,
|> the specification has less errors and/or is more complete and understandable,
|> then it does not really matter whether there exists a miraculous tool that,
|> with a push of a button, will create code out of a specification.
|> 
|> -Haim Kilov
|> haim@dancer.cc.bellcore.com
|> 

Absolutely YES. For trivial systems one may think that writing it down in
a formal methods will allow one to capture the whole problem. For less
simple cases one needs tools to be able to reason about the specification.

Examples: - Syntax and static semantics checkers (nearly allows very experienced
            people make such mistakes, but why spend time on it if a computer
            can help us)
          - Animator or simulator, to animate the behaviour we have written
            down to check our assumptions about the specifications
          - Verification to check whether some properties hold (more
            difficult than animation to make tools because of the inherent
            complexity
          - Report generators, to get a better overview (e.g. graphical
            representation).

Finally compilation will be great, but one must not forget that also bridging 
the gap between first specification (of user-requirements generally) and the
final implementation in hard/software, a lot of human intelligence is needed.

So for thousands of centuries we can learn that the human kind is capable 
of making and using tools, but still we need humans to do both.


    ___
 __/   \__________  Jeroen van de Lagemaat    <lagemaat@cs.utwente.nl>
|  \___/          |         
|___     __   ___ | University of Twente     
| |  |  /  \ (__  | Tele-Informatics & Open Systems
| |__|__\__/____) | P.O. Box 217  NL-7500 AE Enschede  The Netherlands
|_________________| tel. +31 53 893684              tfx. +31 53 333815

                    Humour, you're making me laugh.
                                    - Herman Finkers, Dutch comedian -