Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!mips!sdd.hp.com!hplabs!otter.hpl.hp.com!hpltoad!cdollin!kers From: kers@hplb.hpl.hp.com (Chris Dollin) Newsgroups: comp.lang.misc Subject: Re: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: Date: 17 Apr 91 08:23:38 GMT References: <1954@optima.cs.arizona.edu> Sender: news@hplb.hpl.hp.com (Usenet News Administrator) Organization: Hewlett-Packard Laboratories, Bristol, UK. Lines: 42 In-Reply-To: gudeman@cs.arizona.edu's message of 15 Apr 91 23:47:05 GMT Nntp-Posting-Host: cdollin.hpl.hp.com David Gudeman says: [quote] ] ]Usually not, because the specification is at a higher level and closer ]to the way a person thinks than an implementation. That is an argument for higher-level programming languages (with dynamic typing, for instance), not an argument for adding another language (the specification language) to the process of implementing software. If your specification is so great, why not make that your programming language? [end quote] Because specifications need not be constructive. Consider fn sqrt is sqrt x pre x >= 0 return y post y * y = x [This is a piece of HP-SL, a VDM derivative we're working on.] Any suggestions on how to compile this to code that you'd use in Real Life? Or fn invf is invf (f, f') == (FORALL x. f' (f x) = x) which tests two functions to see if one is the inverse of the other? I'm all in favour of raising the level of programming languages, but the point of a specification language is to describe the intended behaviour without being constrained by the details of a language that is perforce intended to manifest that behaviour on (usually) a sequential machine in (usually) a reasonably short time. [Incidentally, the type-checker tells me that the types of those functions are fn invf : (_A -> _B) -> ((_B -> _A) -> Bool) fn sqrt : Num -> Num Just what I wanted. *In this case*, static type-checking is fine.] -- Regards, Kers. | "You're better off not dreaming of the things to come; Caravan: | Dreams are always ending far too soon."