allen@gitpyr.UUCP (P. Allen Jensen) (08/11/85)
I am doing some research on Program Specification Languages. I am aware of only
two system currently available:
o - Program Statement Language/Program Statement Analyzer (PSL/PSA)
University of Michigan
o - Software Development System (SDS, SREM)
Ballistic Missile Defense and TRW, Inc.
PSL uses Objects and Relationships to describe a system. The language allows
22 possible objects and 36 relationships. These descriptions are then analyzed
by PSA for redundancies or logical inconsistencies. PSA, however, is not
rigorous and therefore cannot provide a mathematically correct verification of
the logical consistency of the specifications.
I am not familiar with SDS, but understand that it is more extensive than
PSL/PSA.
Any further information on currently available products or research in this
area would be appreciated. I am considering developing a prototype language
for specifications in Prolog. All comments and suggestions are welcome.
Allen Jensen
--
P. Allen Jensen
Department of Civil Engineering
Georgia Insitute of Technology, Atlanta Georgia, 30332
...!{akgua,allegra,amd,hplabs,ihnp4,masscomp,ut-ngp}!gatech!gitpyr!allenjbn@wdl1.UUCP (08/23/85)
There have been many attempts at formal specification languages. The idea seems to have originated with Dave Parnas (presently at U. of N. Carolina at Chapel Hill) some years ago. There is a whole methodology out of SRI International called the Hierarchical Development Methodology, with the specification languages SPECIAL (now obsolete) and ORDINARY (unfinished). Most of the SRI work wasn't of very high quality. Don Good's Gypsy project at the University of Texas is the most successful system to date. All of these systems belong to the family of algebraic specification languages, and all suffer from a common problem; specifications of non-trivial systems tend to be large and turgid. In fact, they tend to look a lot like programs. The idea that a tiny specification can exactly specify the behavior of a large program seems not to work. For trivial examples, and for some special cases (sorting, for example) algebraic specifications seem very promising. But the concept doesn't scale up well. I used to do work in the verification area, and verification that code matches specifications, while painfully difficult, is quite possible. But it doesn't seem to be too useful. We need a breakthrough on the specification front. Some people at the Kestrel Institute have been talking about a natural language front end to a specification system, but this is a dumb idea; large formal specifications in natural languages aren't particularly comprehensible either; take a look at what are called ``B-5 specifications'' for military software. I've heard that Kestrel has dropped this idea and is now working on graphical specifications, which may be a useful direction. John Nagle
franka@mmintl.UUCP (Frank Adams) (08/31/85)
The whole idea of a specification language for a computer program is flawed. If the specification is good enough to really determine what the program does, it IS a program; only the compiler is missing. If it isn't that good, why bother with a formal specification language? (Do write a specification, of course; just don't expect it to be good enough for a verification.)
scott@scirtp.UUCP (Scott Crenshaw) (09/05/85)
> > > The whole idea of a specification language for a computer program is flawed. > If the specification is good enough to really determine what the program > does, it IS a program; only the compiler is missing. If it isn't that good, > why bother with a formal specification language? (Do write a specification, > of course; just don't expect it to be good enough for a verification.) I agree. However, I think efficiency considerations play an important part in the current state of affiars. Most specification languages simply can't be translated efficiently enough for production work on current architectures. Furthermore, once a formal specification is validated, implementation issues can be resolved by people whose experience lies in conventional programming languages . There aren't many people experienced in specification languages. -- -- Scott Crenshaw {akgua,decvax}!mcnc!rti-sel!scirtp SCI Systems , Inc. Research Triangle Park, NC
john@chalmers.UUCP (John Hughes) (09/07/85)
In article <629@mmintl.UUCP> franka@mmintl.UUCP (Frank Adams) writes: > >The whole idea of a specification language for a computer program is flawed. >If the specification is good enough to really determine what the program >does, it IS a program; only the compiler is missing. Not so. Many precise specifications aren't programs in any sense - the simplest example is the integer square root function, specified by sqrt(n)*sqrt(n) = n & sqrt(n)>=0 Also, a specification may deliberately avoid stating exactly what the program must do. For example, if "parse" is a function from documents to syntax trees, then a pretty-printer might be specified by parse (pretty tree) = tree This avoids cluttering the specification with unnecessary detail. I recommend looking at some specifications in the Z specification language, developed at Oxford. Z isn't "algebraic" - programs are specified by giving set theoretic models of their behaviour. There are papers on a specification of a (real) screen editor, the UNIX file store, an electronic mail system, parts of a distributed operating system, and others. I'd guess specifications are usually about one tenth the size of the program they specify (very roughly). The man to contact is Bernard Sufrin Oxford University Programming Research Group 8-11 Keble Road Oxford UK sufrin%ox.prg@ucl-cs (.ARPA? .CSNET? .UK?)
peter@yetti.UUCP (Runge) (09/13/85)
> In article <629@mmintl.UUCP> franka@mmintl.UUCP (Frank Adams) writes: > > > >The whole idea of a specification language for a computer program is flawed. > >If the specification is good enough to really determine what the program > >does, it IS a program; only the compiler is missing. > > Not so. Many precise specifications aren't programs in any sense - the > simplest example is the integer square root function, specified by > > sqrt(n)*sqrt(n) = n & sqrt(n)>=0 I think there are probably some good arguments (but not many) for distinguishing between specification and programming languages but Chalmer's "simplest" example of a specification which is not in "any sense" a program is quite unconvincing. Specifications must be taken relative to what is assumed to be already specified. In this case, if we assume an appropriate product relation is available, Chalmer's example becomes a perfectly meaningful program. In a logic-programming environment, there is no reason why sqrt(X,N) if N > 0 and product(N,N,X) cannot evaluate N given a value for X, assuming of course that product(X,Y,Z) can be so specified that its implementation terminates when only Z is instantiated, or if lazy evaluation is available that an appropriate stream of bindings for X and Y is generated. The moral, I think, is that one should try to be as open-minded as possible as to what could constitute a program, and avoid the sterile preconceptions which result from our unfortunate education with conventional programming languages. -- Peter H. Roosen-Runge, Department of Computer Science, York University Toronto M3J 1P3 , Ontario, Canada _____________________________________________________________________________ "Eccles, is the ship sinking?" "Only below the sea." "We must try to save the ship -- help me get it into the lifeboat." _____________________________________________________________________________
os@cstvax.UUCP (Oliver Schoett) (09/30/85)
In article <255@yetti.UUCP> peter@yetti.UUCP (Peter H. Roosen-Runge) writes: > In a logic-programming environment, there is no reason why > sqrt(X,N) if N > 0 and product(N,N,X) > cannot evaluate N given a value for X, assuming of course that product(X,Y,Z) > can be so specified that its implementation terminates when only Z is > instantiated, or if lazy evaluation is available that an appropriate stream > of bindings for X and Y is generated. To say "... so specified that its implementation terminates ..." is to fuse the notions of specification and implementation. Obviously, then, there is no clear distinction left! The purpose of a specification is to characterize the correct implementations. Hence specifications are equivalent iff they admit the same implementations; to distinguish "terminating" and "nonterminating" specifications does not make sense (it's like distinguishing specifications written in black and blue). If you write a specification with operational concerns in mind (termination or efficiency), as you have to in languages such as PROLOG, you are programming. For example, it is misleading to claim that "logic programming notations allow to execute specifications" (Roosen-Runge doesn't do this in his article!)---the writing of "logic programs" is programming. The advantage of such programs over conventional ones might be that they can more easily be read as specifications, i.e., that it might be easier to verify that they produce correct results (when they do!). -- Oliver Schoett UUCP: ... mcvax!ukc!{hwcs,kcl-cs,ucl-cs,edcaad}!cstvax!os ARPA: os%cstvax@ucl-cs.arpa tel: +44 31 667 1081 ext. 2815 mail: Department of Computer Science, University of Edinburgh, The King's Buildings (JCMB), Mayfield Road, Edinburgh EH9 3JZ, Great Britain
jbn@wdl1.UUCP (10/06/85)
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