Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!ub!uhura.cc.rochester.edu!rochester!kodak!islsun!cok
From: cok@islsun.Kodak.COM (David Cok)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1991Apr16.130341.27345@kodak.kodak.com>
Date: 16 Apr 91 13:03:41 GMT
References: <1954@optima.cs.arizona.edu>
Sender: news@kodak.kodak.com
Organization: Eastman Kodak Co., Rochester, NY
Lines: 50

In article <1954@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>In article  <50835@nigel.ee.udel.edu> Darren New writes:
>]
>]>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.
>
>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?
>

Specification languages are and should be different in character than
programming languages.  A specification will state the properties of a
result (given restrictions on the input) or of the state of a system, such
as that a given sequence is ordered.  It says nothing about the method used
to achieve that.  Indeed there are many methods (algorithms) for sorting.
Some of them are quite complex in order to achieve some desired level of
performance.  Different ones will be applicable in different situations.
The question is whether the implementation in the programming 
language actually will produce a result with the desired properties.  It is
my gut feel that for computations which are somewhat close to mathematics
(e.g. sorting), the statement of a predicate giving a specification for a
function can usually be considerably simpler than the statement of an algorithm
for computing the result.  It seems iffier for things like GUIs but that may
be simply a paucity in specification languages. An automated tool which 
will statically produce cases in which the result of a piece of code will not
satisfy the specification would be a valuable contribution to program 
correctness.  

In this context I see program verification in the same light
as testing.  Testing finds bugs; it does not show that a program is correct.
Since specifications can not cover all conditions, a proof of correctness
on code fragments does not show that code compiled with a real compiler 
running on a real machine will execute without error, but if the proof fails, 
it may well point out a case that the code does not handle properly.  Thus 
program verification also serves to find bugs rather than to verify 
correctness.  Since it can be run on the static text, it could point out 
some errors much earlier in the programming process than testing could.
This would be true even if the specifications covered only some aspects of
program logic, leaving out practically important areas such as computation
time, peak memory usage, average paging as a function of physical memory.

David R. Cok
Eastman Kodak Company -- Imaging Science Lab
cok@Kodak.COM