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: <50453@nigel.ee.udel.edu>
Date: 11 Apr 91 21:52:01 GMT
References: <1755@optima.cs.arizona.edu>
Sender: usenet@ee.udel.edu
Organization: University of Delaware
Lines: 83
Nntp-Posting-Host: estelle.ee.udel.edu

In article <1755@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>(1) given that you already think the program is correct by the rules
>of its own notation, why does it increase your confidence just because
>you have another "program" in another notation that says the first one
>is correct?

If by "correct" you mean "meets the specification" then the ability to
show that the behavior of the program is related to the behavior
of the specification is a testing-equivalence sense can be very helpful.

For example, your customer gives you the following requirements:

1) a phone will not ring if it is off-hook.
2) a phone will ring if it is on-hook and its number is dialed.
3) a non-ringing phone will issue a dialtone if off-hook and no
   digits have been dialed.
4) a phone which has had 7 digits dialed will emit either a ring signal
   or a busy signal.
5) ring signals will never be associated with phones which are not ringing.
 
 etc etc etc

Clearly, this is the kind of specification a customer wants to give.
Such a specification, translated into (say) LOTOS, could be used to
find unspecified behavior. For example, the above does not specify that
busy signals won't be sent to phones which are on-hook. Now you can go
to the customer and say "here, formally, is what I think you want.
It's missing this information. Am I correct in your interpretation?"

Once the specification is complete and correct in LOTOS, it is possible
to implement a program in LOTOS. This program, due to circumstances
which I won't explain here, should be written in a style different from
the specification; for example, the specification may be
constraint-based and the "implementation" may be state-machine based.
However, by using the same formalism and the rules of equivalence, it
is possible to show that the state-based version presents the same
external behavior as the constraint-based version.  Now we have an
implementable specification for a phone switch which we know meets the
customer's specifications, which are unambiguous because we made sure
they were unambiguous formally.

Once implemented, if you really, really, really, need assurance that it
is correct, you need to prove that the compiler generated the correct
code, that the CPU correctly interprets the machine code, and so on.
Neither testing nor formal methods will show you that the hardware
is reliable; they only reduce the probability that it is wrong. Both are
appropriate at different levels.

If you want an "informal" language with formal semantics (say, Turing,
which gives formal semantics for a language which looks like an
otherwise pretty standard imperitive language), the formal semantics
allow precise communication between the compiler-writer and the
compiler-user. You can analyze a program and say "if the compiler
behaves as specified, my code can never index off the end of this
array." Alternately, you can turn on runtime checking and test it a few
times to see if it crashes. The difference is: what are you testing?
The compiler, or your code?  I think that all formalisms are purely for
human-to-human communication.  There is no way to formally prove that a
formalism is isomorphic with an informal phenomenon.  The advantage of
using a formalism to communicate is that it provides modularity of
understanding:  1) do you understand the formalism? 2) do you
understand the specification I have written in that formalism? 3) Does
your understanding of what you want match the specification I have
written? 4) Does the implementation behavior match the specification I
have written? By using the right level of detail/abstraction/whatever
at each level, interpersonal communication can proceed quite quickly
and accurately.  Only step (4) really needs informal testing; I can't
imagine how you could "test" a specification of what is wanted.

One of the grad students here managed the implementation of a network
protocol with some sophisticated bandwidth-reduction mechanisms.  He
learned Estelle (a formalism for specifying protocols) about half-way
through the project.  He says that if he knew Estelle at the start, he
could have cut development time in half, not because Estelle is so
great, but because it is easier to communicate precise and accurate
protocol details in Estelle than in English. Formalisms are just
jargon; if you know them, they really speed up communication, but they
don't mean that what you said is right.

-- 
--- Darren New --- Grad Student --- CIS --- Univ. of Delaware ---
----- Network Protocols, Graphics, Programming Languages, FDTs -----
+=+=+ My time is very valuable, but unfortunately only to me +=+=+