On Tue Sep 27, 2005 at 17:01:55 +1000, QuantumG wrote: > >Speaking of static analysis. I managed to get an evaluation version of >this software: > > http://www.eschertech.com/products/ > >It works by changing the level of representation at which you write >software. Instead of writing imperative programs you write declarative >specifications. The problem is it's: > > 1. a new, unfamiliar and difficult to master syntax (and way of >thinking). > 2. useless for already developed software. > 3. limited in obscure and unobvious ways. > >In particular, you can write a full and complete specification, ask it >to generate a program which implements that specification and it will >barf. You've done everything that should be required but the state of >the art of specification refinement that Perfect Developer embodies is >not sufficient to generate code for any given specification. So you >have to write code to do the "hard bits" of the specification, stating >how the program should operate, not just what the program should do. >That'd be fine if you could do it in a real programming language, but >instead you've gotta use the specification language. Programming in a >specification language is much like chinese water torture. > >But it gives you an idea of just how extreme static analysis can be. >You literally can write some specifications in Perfect Developer that >can be verified for internal consistency, automatically refined into a >working prototype with good performance and deployed as is. Maybe in 10 >years time all critical systems will be written with tools like this? >Maybe in 20 years time all other software will be written with tools >like this?
There is also Isabelle: http://isabelle.in.tum.de/ which is free. And there is current work attempting to use such an approach to generate a verified operating system kernel: http://www.cse.unsw.edu.au/~formalmethods/projects/l4.verified/ There is also splint, but that is a more traditional static analysis tool. Benno -- SLUG - Sydney Linux User's Group Mailing List - http://slug.org.au/ Subscription info and FAQs: http://slug.org.au/faq/mailinglists.html
