A boss of mine at Bellcore, and a very smart guy (B. Gopinath) once mentioned to me that (with the exception of scheme) he'd never seen a set of formal semantics for a language that were smaller than the largest program one would care to write in the language.

I suggest he look at occam, the semantics are very compact, about ten pages. The purpose of writing the denotational semantics is to obtain a grounding for the axiomatic semantics which may then be used for proofs. All this means is that languages such as ADA are useless for formal methods work because the language is too big to develop a usefull semantics for it. C is better but still far too large and the semantic ambiguities of the language cause problems. I don't consider the conventional application of formal methods to be a practical approach. This does not mean that no such approaches exist, merely that people use the wrong ones. Phill H-B