Path: utzoo!attcan!uunet!samsung!zaphod.mps.ohio-state.edu!usc!apple!voder!pyramid!athertn!joshua
From: joshua@athertn.Atherton.COM (Flame Bait)
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Message-ID: <19989@joshua.athertn.Atherton.COM>
Date: 19 Mar 90 17:47:03 GMT
References: <12326@goofy.megatest.UUCP> <18261@duke.cs.duke.edu>
Reply-To: joshua@Atherton.COM (Flame Bait)
Organization: Atherton Technology, Sunnyvale, CA
Lines: 24

In article <18261@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes:
>I don't *think* a formal proof is a good way to budget test time, I have
>evidence from controlled studies and anechdotal evidence that says it
>is.  

Can you please post 3-6 references to the controlled studies which show
that formal proofs are a better way to budget time than debugging?

For these studies to be really convincing (to me, anyway) they should
involve real world software projects, in real world environments.  The
projects should be on "normal" hardware (no LISP machines, Butterflies,
or connection machines).  I should be able to buy or otherwise aquire 
all the speciallized software used.  I should be able to take classes
in the methodology used.  The studies should compare projects which 
use good SE methodology (without proofs) to good SE methodology (with
proofs).  

Remember: in the commerical world, something only exists if I can buy it.

Obviously, I'd be very interested in studies which do not match all of
the above requirements, but the more they match, the better they are.

Joshua Levy                          joshua@atherton.com  home:(415)968-3718
                        {decwrl|sun|hpda}!athertn!joshua  work:(408)734-9822