Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!rpi!batcomputer!cornell!oravax!ian
From: ian@oravax.UUCP (Ian Sutherland)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1249@oravax.UUCP>
Date: 17 Jan 90 17:18:11 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP> <1928@uwm.edu> <11810@cs.yale.edu>
Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland)
Organization: Odyssey Research Associates, Ithaca, New York
Lines: 34

In article <11810@cs.yale.edu> blenko-tom@CS.YALE.EDU (Tom Blenko) writes:
>	How do you ensure that the specification is any good?

This is a question which is very germane to formal verification.  I've
seen a lot of formal specifications that didn't say what their author
meant them to say because he wasn't sufficiently careful with his use
of first order logic.

There are several potential ways of addressing the problem of correct
formal specifications.  The most obvious way is to get people to write
the specifications who know how to read and write first order logic (or
whatever kind of formal language you're using).  Another way would be
to come up with declarative languages with a formal semantics which are
more perspicuous than first order logic.  Yet another way is to come up
with generic specifications of particular system properties that you
want to verify about many systems.  The particular example of this last
that I've done a lot of work on is the property of being secure, in the
sense that information of a particular classification cannot be
inferred by an entity whose classification is not greater than or equal
to that of the information.

>       I have
>	worked with specifications in industry, and I'm sure I've never
>	seen one that was complete. I probably have never seen one that
>	is both non-trivial and consistent. So where do you get good
>	(consistent and reasonably complete) specifications?

Would you say what you mean by "consistent" and "complete"?  These are
very overloaded words.

-- 
Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Sans Peur