Crispin wrote: >> Here's an example of a case it cannot prove:

if X then Y <- initial value endif ... if X then Z <- Y + 1 endif The above code is "correct" in that Y's value is taken only when it has been initialized. But to prove the code correct, an analyzer would have to be "flow sensitive", which is hard to do. << The whole science of program proving is based on exactly this sort of flow analysis. The analyser will postulate that Y is initialised at the assignment to Z, given the deduced program state at that point. This is called a "verification condition" or "proof obligation". It can then attempt to prove the hypothesis; for this example, the proof is trivial. I guess it would have been more difficult 20 years ago when Hermes was written. The alternative solution to the problem of uninitialised variables is for the language or static checker to enforce Java's "definite initialisation" rule or something similar. This at least guarantees predictable behaviour. An issue arises when a tool like Perfect Developer is generating Java code, because even though PD can prove that Y is initialised before use in the above example, the generated Java code would be violate the "definite initialisation" rule. We have to generate dummy initialisations in such cases. David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com