On Nov 13, 2005, at 12:21 PM, Marianne Susaanti Follingstad wrote:
So what is this "underlying theory," Greg?
The short answer is model theoretic semantics. The long answer may have to wait a bit, but it is rather stunning to me (at least) how broad a range of problems in program logics are decidable (with manageable complexity). The upshot of that is that it really is practical to describe software at a higher level of abstraction than that to which we are accustomed and generate provably correct solutions. That was really my point: though we cannot hope to come up with a general purpose algorithm for program verification, we can develop verifiable solutions for restricted classes of problems that are still general enough to be of practical use.
=== Gregory Woodhouse [EMAIL PROTECTED] "The universe is not required to be in perfect harmony with human ambition." --Carl Sagan ------------------------------------------------------- SF.Net email is sponsored by: Tame your development challenges with Apache's Geronimo App Server. Download it for free - -and be entered to win a 42" plasma tv or your very own Sony(tm)PSP. Click here to play: http://sourceforge.net/geronimo.php _______________________________________________ Hardhats-members mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hardhats-members
