Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sun-barr!lll-winken!elroy.jpl.nasa.gov!swrinde!zaphod.mps.ohio-state.edu!wuarchive!uwm.edu!ux1.cso.uiuc.edu!midway!midway!stephen From: stephen@estragon.uchicago.edu (Stephen P Spackman) Newsgroups: comp.lang.misc Subject: Re: Formal definitions and other fantasies Message-ID: Date: 3 May 91 10:31:35 GMT References: <2202@optima.cs.arizona.edu> <1991Apr19.234958.9400@kodak.kodak.com> Sender: news@midway.uchicago.edu (NewsMistress) Organization: University of Chicago CILS Lines: 23 In-Reply-To: cok@islsun.Kodak.COM's message of 19 Apr 91 23: 49:58 GMT One interesting thing that Hendrik Boom mentioned to me from using his (total correctness) verifier was that he typically found more bugs in his SPECIFICATIONS than he did in his PROGRAMMES (for example, a sort routine failed to typecheck because the specification failed to handle duplicates correctly). Now, you might think that this is a strike against verification (at very least it suggests that writing short, abstract, mathematical specs may NOT be easier than coding up a decent algorithm, and that checking such a spec by eye may not be so straightforward), but in fact it's precisely the spec (albeit in a less formal form) that is going to be the interface contract between the routine and the outside world. The effect of the verifier, then, is to make you look VERY hard at the properties of your interfaces. And my experience has been that interfaces are the things that HAVE to be right - the code you can always discard. ---------------------------------------------------------------------- stephen p spackman Center for Information and Language Studies systems analyst University of Chicago ----------------------------------------------------------------------