@LoopInvariant annotation

[leouk]

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

[nickbattle]

If you can give me a suggested form for the annotation, I can have a go at creating one. But remember annotations were intended to be user-provided, so perhaps this (and other proof-related annotations) ought to be in the VDM_Toolkit rather than within VDMJ's standard annotation library?

[leouk]

Hi Nick, I considered that as well (i.e. be a VDM_Toolkit thing). But then I realised that VDM has measures for functions, but not for loops/operations. In the case of loops, I presumed this was something akin to user formal documentation. The "shape" of it is that of @LoopInvariant(boolean-expression), where whenever the loop guard is true, the expression must also be true. Arguably one can also think of @LoopVariant(nat-expression), where this is like a measure for loops? But fair enough, I will think about adding this to VDMToolkit annotations.

[nickbattle]

Hmm. I see your point though: there is no measure for operations. I should be fairly simple to create such an invariant annotation anyway. Perhaps if you create one, then we can look what whether it's useful enough to include in the standard annotations jar?