Nick Battle

Many thanks for the FMPy walkthrough today. I was particularly interested to see how you did the XML validation (and perhaps how you could do dynamic API validation), comparing this...

> These check are quite expensive if you perform them every time. Yes, of course. But the formal model is trying to define what the rules are, rather than producing...

It should be fairly simple to walk the tree and look for various con/disjunctions in expressions. But where would an annotation "keep" that result? Or did you mean that annotations...

Maybe better to discuss this by email :-)

The "measure" function within a FunctionValue is looked up on the fly, presumably as a hangover from being able to specify measures as the name of a function rather than...

The expression and/or statement finders need to be enhanced to "find" the expression body of the assignment definition (the dcl). Just fixing that may be enough to solve this issue....

​Well, the first thing​ to say is that none of this behaviour is particularly well defined anywhere! I would quibble about whether B's constructor overrides A's (if that's what you...

If you try this with VDMTools (I'm using 9.0.3 Linux), then the specification typechecks cleanly. You can then create instances of B, either as B() or B(1), but you cannot...

I think the "default default" module is just the first in the list of modules build by the parser. In VDMJ, that is the order of the modules in the...

I agree it would be nice. It applies to VDM++ too (there is a default class). The option only makes sense for the Console mode though, so it ought to...