Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!uunet!mcsun!ukc!ox-prg!bowen
From: bowen@prg.ox.ac.uk (Jonathan Bowen)
Newsgroups: comp.software-eng
Subject: Re: Modifiability
Message-ID: <1841@culhua.prg.ox.ac.uk>
Date: 11 Jun 91 09:15:00 GMT
References: <11714@ncar.ucar.edu> <1991Jun7.165928.1903@weyrich.UUCP> <1849@uqcspe.cs.uq.oz.au> <1991Jun10.122656.18795@zip.eecs.umich.edu> <1991Jun10.174641.8176@netcom.COM>
Sender: news@prg.ox.ac.uk
Reply-To: Jonathan.Bowen@prg.oxford.ac.uk (Jonathan Bowen)
Distribution: comp.software-eng
Organization: Programming Research Group, Oxford University, UK
Lines: 72

In article <1991Jun10.174641.8176@netcom.COM> jls@netcom.COM (Jim Showalter) writes:
>>I'd assert, however, that
>>more than 95% of a reasonably sized program's code is an attempt at writing
>>a non-ambiguous specification. 1/2 :-)
>
>Excellent point, and a great way to succintly express my dissatisfaction
>with formal specification languages. I have seen such languages work well
>in a restricted domain (e.g. state transition tables), but in the larger
>scheme of things they either wind up too specific for the general case,
>or so general they are no longer concise.
>
> ...
>
>I think there is a lesson here for anyone who wants to specify systems
>in a formal language--it may well be the case that any time one wants
>to formally specify a system of suitable complexity to be interesting,
>the resulting specification language is itself so complex that it provides
>scant improvement over English or, alternatively, the language of 
>implementation itself.

You might be interested in the work at IBM, Hursley Park, in the UK.
They have specified part of CICS (a commercial transaction processing
system) in the formal specification notation Z and have coded (or
recoded) 100,000+ lines of program from these specifications.  The
overall development cost and number of errors detected have been
reduced, although there are significant (one-off) educational costs to
retrain employees. See the following reference for further details:

@article{Z:Nix88,
  author = {C.J. Nix
    and B.P. Collins},
  title = {The use of Software Engineering, including the {Z} Notation,
    in the Development of {CICS}},
  journal = {Quality Assurance},
  volume = {14},
  number = {3},
  pages = {103-110},
  month = {September},
  year = {1988}
}


You should also look at the September 1990 special issue of IEEE
Software on formal methods; in particular:

@article{Z:Hall90b,
  author = {Anthony Hall},
  title = {Seven Myths of Formal methods},
  journal = {IEEE Software},
  pages = {11-19},
  month = {September},
  year = {1990},
  annote = {
    Formal methods are difficult, expensive, and not widely useful,
    detractors say. Using a case study and other real-world examples,
    this article challenges such common myths.}
}

The following myths are systematically covered:

 * Formal methods can guarantee that software is perfect.
 * They work by proving that programs are correct.
 * Only highly critical systems benefit from their use.
 * They involve complex mathematics.
 * They increase the cost of development.
 * They are incomprehensible to clients.
 * Nobody uses them for real projects.


--
Jonathan Bowen, <Jonathan.Bowen@prg.oxford.ac.uk>
Oxford University Computing Laboratory.