hjm@cernvax.UUCP (hjm) (07/25/88)
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
daveb@geac.UUCP (David Collier-Brown) (07/28/88)
From article <781@cernvax.UUCP>, by hjm@cernvax.UUCP (hjm): > 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? Well, for certain well-specified things, my implementations are taken directly from formal specifications, or from composing the specifications of several parts to make a new whole. This can be a real time-saver, especially If you collect formal (algebraic, mostly) specs. I only do about 10% this way, mostly because I'm better at using specs than writing them... Currently I'm reading Wladislaw M Turski & T.S.E. Maibaum's "The Specification of Computer Programs" (Addison-Wesley, 1987), in hopes of improving the odds. --dave (I also use WEB) c-b -- David Collier-Brown. {mnetor yunexus utgpu}!geac!daveb Geac Computers Ltd., | Computer science loses its 350 Steelcase Road, | memory, if not its mind, Markham, Ontario. | every six months.