From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,a83c46b54bacb7f6 X-Google-Attributes: gid103376,public From: Rod Chapman Subject: Re: JOB:Sr. SW Engineers Wanted-Fortune 500 Co Date: 2000/02/02 Message-ID: <3897F502.1484544E@praxis-cs.co.uk>#1/1 X-Deja-AN: 580735338 Content-Transfer-Encoding: 7bit References: <3894A823.92EC75D1@bondtechnologies.com> <874b7r$mj9$1@nnrp1.deja.com> <877081$knt$1@nnrp1.deja.com> X-Accept-Language: en Content-Type: text/plain; charset=us-ascii X-Trace: 2 Feb 2000 09:09:23 GMT, 193.114.91.187 MIME-Version: 1.0 Newsgroups: comp.lang.ada Date: 2000-02-02T00:00:00+00:00 List-Id: > When you develop pacemaker software in Ada, you still must scrutinize the > code to insure that runtime exceptions will never happen. There's an alternative...we now have the tools do construct proofs that exceptions are never raised, and thus we can _justifiably_ turn off checks. Proofs are (given some reasaonable failure hypothesis) valid for all input data. It also (surprisingly) turns out that the proof work was _more_ cost effective than unit testing on one project - see our paper in FM'99 for details. This stuff really works, and we've done it on several large projects, mostly in the safety-critical aerospace arena. Most people seem to think that program proofs on reasonable size projects is impossible, perhaps owing to bad experiences on University courses (just like me!) - Rod Chapman