Path: utzoo!attcan!uunet!mcvax!cernvax!hjm
From: hjm@cernvax.UUCP (hjm)
Newsgroups: comp.software-eng
Subject: Formal methods - does anyone use them?
Message-ID: <781@cernvax.UUCP>
Date: 25 Jul 88 10:09:23 GMT
Reply-To: hjm@cernvax.UUCP (Hubert Matthews)
Distribution: comp.software-eng
Organization: CERN European Laboratory for Particle Physics, CH-1211 Geneva, Switzerland
Lines: 18

The subject of formal methods was brought up recently (VDM, Z et al.), and I
was wondering to what extent people use these methods on 'real' projects.  Do
people just use them for the design phase and then just code it normally, or do
they refine the mathematical description until it turns into executable code?
Also, does anyone use such techniques for producing a 'runnable specification'?
I've seen some work on this, with people translating Z into PROLOG and also
investigating the behaviour of a system defined in Hoare's CSP using a PROLOG
trace package.

This is just an informal query as I would like to get some pointers to other
work in the literature so that I can keep up to date.  Therefore, I would
appreciate any references that people would send me, as /* flame on */ I 
consider software eng. to be a formal approach and not just drawing pretty
pictures /* flame off */.

	Hubert Matthews

"OK, so it works - now prove it!" - Tony Hoare to one of his research students