Dag-Erling Smorgrav wrote:
>
> Correctness proofs are very time-consuming, because they can't be
> automated. There are experimental tools which can assist with part of
> the work (e.g. the partially-completed Abel project at the University
> of Oslo: <URL:http://www.ifi.uio.no/~prover/abel/>) but the hardest
> part of the job - finding loop and type invariants and post- and
> pre-conditions which the prover can use as starting points - must
> still be done manually.
Things like SPIN goes a long, long way to make such proofs more
viable. Take, for instance, correctness proofs of Fluke IPC
subsystem.
--
Daniel C. Sobral (8-DCS)
d...@newsguy.com
d...@freebsd.org
"Proof of Trotsky's farsightedness is that _none_ of his
predictions have come true yet."
To Unsubscribe: send mail to majord...@freebsd.org
with "unsubscribe freebsd-hackers" in the body of the message
