David Hopwood wrote: > Marshall wrote: > > > Wouldn't it be possible to do them at compile time? (Although > > this raises decidability issues.) > > It is certainly possible to prove statically that some assertions cannot fail. > > The ESC/Java 2 (http://secure.ucd.ie/products/opensource/ESCJava2/docs.html) > tool for JML (http://www.cs.iastate.edu/~leavens/JML/) is one system that does > this -- although some limitations and usability problems are described in > <http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/papers/CASSIS2004.pdf>.
I look forward to reading this. I read a paper on JML a while ago and found it quite interesting. > > Mightn't it also be possible to > > leave it up to the programmer whether a given contract > > was compile-time or runtime? > > That would be possible, but IMHO a better option would be for an IDE to give > an indication (by highlighting, for example), which contracts are dynamically > checked and which are static. > > This property is, after all, not something that the program should depend on. > It is determined by how good the static checker currently is, and we want to > be > able to improve checkers (and perhaps even allow them to regress slightly in > order to simplify them) without changing programs. Hmmm. I have heard that argument before and I'm conflicted. I can think of more reasons than just runtime safety for which I'd want proofs. Termination for example, in highly critical code; not something for which a runtime check will suffice. On the other hand the points you raise are good ones, and affect the usability of the language. Marshall -- http://mail.python.org/mailman/listinfo/python-list