Leo Freitas

@spec(name[, weight]) annotation

2

Nick, I wanted to suggest a new annotation. I thought to implement it in VDM_Toolkit but then wanted to share it here for thoughts/comments (or warnings!). :-) A while ago...

@LoopInvariant annotation

3

For loop statements, a loop invariant annotation would be useful for further proof of termination and translation to Isabelle.

Crash during debugging session if change in breakpoints

4

Every time in a debug session, if you change breakpoint locations or enable/disable them, even if through the "BreakPoints" view, Overture crashes.

POG PO source

3

When calling the POG, it would be useful to get location information associated with each of the POs.

Translator erro message output

5

Hi Jonas, Wondered how/where the translation error messages would appear in the extension? Couldn't quite find where they were. Best, Leo