Re: No Go To's Forever!

[Robert Dewar <robert_dewar@my-deja.com>]

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.