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,
	MSGID_RANDY autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,14f7200925acb579
X-Google-Attributes: gid103376,public
From: Robert Dewar <robert_dewar@my-deja.com>
Subject: Re: No Go To's Forever!
Date: 2000/04/01
Message-ID: <8c50hn$hvb$1@nnrp1.deja.com>#1/1
X-Deja-AN: 605249410
References: <8bbsc6$aes$1@nnrp1.deja.com>
 <HRkC4.1999$U95.38761@news.pacbell.net> <8bdbof$t19$1@nnrp1.deja.com>
 <38E1F6D5.8303903C@dowie-cs.demon.co.uk>
 <874s9p7jwi.fsf@deneb.cygnus.argh.org> <8bu48a$3tt$1@nnrp1.deja.com>
 <wcczorgbgwi.fsf@world.std.com>
X-Http-Proxy: 1.0 x33.deja.com:80 (Squid/1.1.22) for client 205.232.38.14
Organization: Deja.com - Before you buy.
X-Article-Creation-Date: Sat Apr 01 14:19:44 2000 GMT
X-MyDeja-Info: XMYDJUIDrobert_dewar
Newsgroups: comp.lang.ada
X-Http-User-Agent: Mozilla/4.61 [en] (OS/2; I)
Date: 2000-04-01T00:00:00+00:00
List-Id: <comp.lang.ada>

In article <wcczorgbgwi.fsf@world.std.com>,
  Robert A Duff <bobduff@world.std.com> wrote:
> Robert Dewar <robert_dewar@my-deja.com> writes:
>
> > On the other hand, you can prove certain properties of a
program
> > without a spec, e.g. that it terminates for all inputs, or
that
> > it cannot raise an exception etc.
>
> To me, that seems like a more useful approach in most
> circumstances.

I would have said more practical. Obviously it is more useful
if you can indeed prove your program meets the formal
specification, but often no such exists, or it is infeasible
to carry out the full proof. On the other hand, tasks like
the ones mentioned above may be feasible even if both these
conditions hold :-)

That is why proof of correctness techniques are a valuable tool
that all programmers should have a good awareness of, even if
you are not in situations where full proofs are feasible.

Unfortunately, especially in this country, things are better
in Europe, too many programmers are allergic to formalism, and
lack the necessary training.


Sent via Deja.com http://www.deja.com/
Before you buy.