Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!uwm.edu!ux1.cso.uiuc.edu!ux1.cso.uiuc.edu!m.cs.uiuc.edu!render
From: render@m.cs.uiuc.edu
Newsgroups: comp.object
Subject: Re: Reasons why you don't prove your pr
Message-ID: <77500024@m.cs.uiuc.edu>
Date: 17 Jan 90 01:38:13 GMT
References: <7578@hubcap.clemson.edu>
Lines: 32
Nf-ID: #R:hubcap.clemson.edu:7578:m.cs.uiuc.edu:77500024:000:1551
Nf-From: m.cs.uiuc.edu!render    Jan 16 10:48:00 1990


Written 12:41 pm  Jan 15, 1990 by joshua@athertn.Atherton.COM:
>No problem.  Specifiy the following programs, in a machine readable
>format useful to a program verifier.  These should be commerical products,
>so they must look good and feel good so that people want to use them:
>
>   A source code control facility like SCCS or RCS
>       If you use system calls you must have some way of proving that
>       they do what your spec says they do.

For this, you might take a look at:

	Ian D. Cottam, "The Rigorous Development of a System Version 
	Control Program," IEEE Transactions on Software Engineering,
	Vol. SE-10, No. 2, March 1984, pp. 143-154.  

I think you'll find basically what you've asked for.  

>My last example points out a current problem with proving program correct.
>They must only use libraries which have been proven correct, must run on 
>an operating system which has been proven correct, and must use hardware
>which is proven correct.  All of this is impossible right now.

Yes, it is impossible to prove anything COMPLETELY correct.  This is because 
the machines and programs involved in doing so are all devised by humans, and
humans are notoriously unreliable.  It is, however, very possible to increase 
one's assurance that a given program is correct using formal program develop-
ment and/or verification techniques.   The benefits of such assurances to 
mission critical software and systems should be obvious.  Thus, continued
research into formal development and proving methods seems quite worthwhile.

hal.