Peter W. V. Tran-Jørgensen

Since VDM is unlimited precision, changing the language to address this issue feels wrong. That being said, I do agree that a notation for expressing limits could be useful. Just...

I'm not sure, but my point is just that you could use it to implement the same functionality that a new language feature would contribute. Syntax validation would be helpful,...

Thanks! I'm happy to hear that you find the tools useful! Please help me understand, if there's no human present at the time why may a warning not be appropriate?...

Related to #466 Thanks for looking into this. I agree, I think it's reasonable to do what you are suggesting.

What's the best solution for this? Do we normalise/denormalise the message before sending/receiving it (in order to get rid of problematic characters), or do we simply disallow these characters when...

For your example only a single error is reported. ``` TypeChecker.report(3325, "Mismatched compose definitions for " + composeType.getName(), composeType.getLocation()); ``` ``` [Error 3325: Mismatched compose definitions for R in 'DEFAULT'...

The current setup also causes problems for a module that wants to implement command-line support and which already has a interpreter dependency. For example, the codegen module needs the interpreter...

I'm not sure how this is handled so I would need to check the code. Anyway, I need to make sure I understand what you are saying. Are you suggesting...

Once the trace has been expanded we could store the resulting `TestSequence` in a map that associates trace definitions with test sequences. Then, if the user sends a test to...

Yeah I'm not sure how easy it is to re-run the tests if we only have the XML. I guess I would need some way to rebuild the test (`CallSequence`?)...