Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!udel!ee.udel.edu
From: new@ee.udel.edu (Darren New)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <50835@nigel.ee.udel.edu>
Date: 15 Apr 91 22:00:24 GMT
References: <1882@optima.cs.arizona.edu>
Sender: usenet@ee.udel.edu
Organization: University of Delaware
Lines: 33
Nntp-Posting-Host: estelle.ee.udel.edu

In article <1882@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>But the "specification" is an
>informal description of what the program should do.  

I'm arguing that formally-specified languages should be used so that
the "specification" can be made formal and then be formally compared
to the "code".

>A _formal_
>specification can be as wrong as a program can.  

Usually not, because the specification is at a higher level and closer
to the way a person thinks than an implementation.  Compare the 
specification of a relational database schema and an RDBMS implementation.
Which is the customer more likely to get right?

>And in general the
>process of writing a formal specification can be a buggy as the
>process of writing a program.

It can be, but experience has again and again shown that formal
specifications tend to have fewer bugs than informal specifications.
See any FORTE conference proceedings.  Every time I've heard of that
somebody has taken (say) an ISO network protocol specification and
respecified it formally, bugs have been found. I consider this a
positive benefit.
			     -- Darren

-- 
--- Darren New --- Grad Student --- CIS --- Univ. of Delaware ---
----- Network Protocols, Graphics, Programming Languages, FDTs -----
     +=+=+ My time is very valuable, but unfortunately only to me +=+=+
+=+ Nails work better than screws, when both are driven with screwdrivers +=+