Re: [SLUG] Re: dynamic vs static type checking

[Benno <benjl@xxxxxxxxxxxxxxx>]

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