Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site wdl1.UUCP
Path: utzoo!linus!decvax!ucbvax!ucdavis!lll-crg!dual!qantel!hplabs!hpda!fortune!wdl1!jbn
From: jbn@wdl1.UUCP
Newsgroups: net.ai
Subject: Re: Re: Program Specification Languages
Message-ID: <736@wdl1.UUCP>
Date: Sat, 5-Oct-85 21:21:21 EDT
Article-I.D.: wdl1.736
Posted: Sat Oct  5 21:21:21 1985
Date-Received: Sat, 12-Oct-85 06:01:35 EDT
Sender: notes@wdl1.UUCP
Organization: Ford Aerospace, Western Development Laboratories
Lines: 26
Nf-ID: #R:mmintl:-62900:wdl1:1100024:000:1156
Nf-From: wdl1!jbn    Oct  5 17:36:00 1985


      There seem to be two schools of thought on formal specification.
One school holds that the specification should contain enough information
to exactly determine what the output of the system should be for any input.
Parnas, Robinson, and their successors in the algebraic specification field
follow this model.

      The other school proposes a looser approach; as with the

	tree = parse(input)

example given above.  Here we are assuming an agreed-upon meaning for
``parse''.  The idea is to have a large supply of objects for which we have
agreed upon meanings.

      So far, we've learned that the first approach leads to specifications
that are smaller than the code, but not an order of magnitude smaller;
for real systems, a factor of two to four seems to be achieved in practice.
(We specified the V6 UNIX kernel in SPECIAL here some years ago as an 
exercise, which is where we discovered this.)  The second approach leads one
off in the direction of rapid prototyping systems, with a very rich supply
of predefined objects which are not particularly efficient but are general.
The larger Lisp systems fit this model.

      				John Nagle