Write it right or right the wrongs?
March 2005
In the continued search for ways of making systems that we can really
trust, there's long been two opposing trends: pushing for better
techniques and tools to produce software that will work the first time
around ("Write it right"); and hoping for tools that, accepting programs
have bugs, will catch them ("Right the wrongs").
Forty years ago (following some early insights of Alan Turing)
researchers started to investigate "program proving". After a while they
accepted that you can't prove a program unless it's been written right
from the start with that goal in mind; and it seemed, in research at
least, that the "a priorists" had gained the upper hand. All the while,
however, tools for static analysis and debugging continued to improve.
Eiffel is firmly into "Write it right", with its constant emphasis on
design principles, on contracts, on structure. I noted in my last column
how bizarre I find the idea of expecting software to be written any good
old way, and then having some magical tool extract the contracts for
you. Of course the "Right the wrongs" part is there too, as with the
sophisticated debugger of EiffelStudio (watch for new advances in
forthcoming versions) and the work done at ETH to generate tests
completely automatically from contracts.
The field will for still quite some time need to rely on both
approaches. For those readers of EiffelWorld interested in following the
progress in the field, let me point out a milestone event that will take
place in Zurich in October (10-13) and to which there is still time to
submit a position paper: the conference on Verified Software: Theories,
Tools, Experiments ETH Zurich, 10-13 October 2005
http://vstte.ethz.ch.
The conference is the brainchild of Tony Hoare as part of his relentless
efforts to start a "Grand Challenge"
on software verification. It is an official IFIP conference,
specificially its Technical Committee 2 (Software) and more specifically
still its Working Group 2.3 (Programming Methodology).
The event is part of an extensive program of celebrations for the 150th
anniversary of ETH Zurich. Sponsors include ETH, Microsoft Research and
the US National Science Foundation.
The roster of organizers and invited speakers reads like a who's who of
the pioneers and innovators in formal methods, program proving, model
checking, abstract interpretation, program refinement etc. I know that
it will be a watershed event.
The conference is by invitation only and the number of seats is limited.
The best way to get invited is
to submit a position paper (click "Submit" at http://vstte.ethz.ch). It
would be great to have a few position papers from the readers of this
newsletter, showcasing their Eiffel experience.
In the meantime, continue to write it right, but don't forget all the
same to chase the wrongs.
--Bertrand Meyer
|
