Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!samsung!usc!apple!sun-barr!newstop!texsun!csccat!larry
From: larry@csccat.UUCP (Larry Spence)
Newsgroups: comp.ai
Subject: Re: Program verification is a proven concept
Message-ID: <3471@csccat.UUCP>
Date: 16 Jan 90 01:08:17 GMT
References: <7578@hubcap.clemson.edu> <25711@cup.portal.com> <1888@uwm.edu>
Reply-To: larry@csccat.UUCP (Larry Spence)
Organization: Computer Support Corporation. Dallas,Texas
Lines: 27

In article <1888@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins) writes:
>I must've missed the boat: I always prove my programs correct. 

Could you give us some examples?  What is the largest program you have
proven correct?  How long did the design and proof process take?  Are these
programs applications that are used by others, or academic exercises?

>Programs in even languages like C, Pascal can be manipulated via a set of
>(complete) algebraic rules -- which form a foundation for the semantics
>of the language in question.

Can you give us pointers to literature (or examples of your own) where a
real-world C program of more than a few dozen lines (i.e., including side-
effects from pointers, aliasing, etc.) is manipulated in a non-trivial
manner (you get to define "non-trivial") via such a set of rules?  

Do any of your "correct" programs use floating point arithmetic (or fixed-
point, for that matter)?  Can such programs be proven correct?

Would you maintain that real-world applications other than those which
MUST be correct at any cost (e.g., space missions, medical apps) SHOULD
be proven correct?  Do you think that this would be cost-effective?

-- 
Larry Spence
larry@csccat
...{texbell,texsun,attctc}!csccat!larry