i'm not clear on what all functional correctness entails. can a functionally correct program suffer from deadlock or livelock?
Yes. It depends on if that property was stated as part of the specification of what correctness means. That is definitely something that can be stated and proven. I'm not sure if their spec stated that correctness means no deadlocks or if they explicitely stated that as a property and then proved it. The spec is publically available but I havent studied it. The proofs are not yet available. There are some papers that talk about some of what they have done.
- erik
Tim Newsham http://www.thenewsh.com/~newsham/
