NetNews Usenet Archive 1992 #31/NN_1992_31.iso/spool/comp/programm/3374

Internet Message Format | 1992-12-30 | 2.4 KB

Path: sparky!uunet!pipex!bnr.co.uk!uknet!comlab.ox.ac.uk!ke94002
From: [e-mail] (Daniel J Mitchell)
Newsgroups: comp.programming
Subject: Re: Programming by Description of Output...
Message-ID: <[e-mail]>
Date: 30 Dec 92 23:36:59 GMT
References: <[e-mail]> <[e-mail]> <[e-mail]>
Organization: Oh, come /on/..
Lines: 46
Originator: ke94002@black


 This method of programming is usually called 'deriving programs'
-- the original work is Edsger Dijkstra's _A Discipline of
Programming_ (Prentice-Hall, 1976), other books I've read which
are probably worth looking at are _Programming from Specifications_
(Carroll Morgan, Prentice-Hall, and the course book for the course
I just did in exactly this subject.. <grin> ), and _The Science of
Programming_ (D.Gries, Springer-Verlag). (Morgan is more concrete
in it's applications, Gries is more abstract).

 To take the example given, sorting, it'd be (in the notation used
in the above, at any rate):

 var a:seq_{N} Z; con A; and A=bag a
 a:[true, up a]

 This then uses the bag abstraction to ensure the elements remain
constant -- there is no precondition, as the data being used here
specifies everything necessary (ie it's a sequence of numbers), and
the postcondition is that the sequence is an upsequence (ie is
sorted).

 This method has some advantages -- if the program is derived
step-by step from the specification to the final code, and each step
is right, then the final code is guaranteed to be correct -- this
is useful in some cases (ie to be sure that, say, a binary search
will find exactly what you want it to find, and not the element one
to the left). Also, the methods used to derive programs are
designed to make it very easy to locate flaws in the derivation if
they exist.

 It also can wind up deriving /very/ elegant algorithms (qv the
longest upsequence problem, covered in Gries and Morgan) for
difficult problems.

 The disadvantage, obviously, is that it takes a lot more time than
it would to just write code in the majority of cases..

 As to doing it automatically, the only thing I know of is a
language called ML which reputedly is a great deal higher level
than most languages, and comes close to being able to take
specifications of the above form as code. (I think. I'm probably
wrong about that, on reflection..)

--
Daniel Mitchell == [e-mail] == bi furry juggler