@spec(name[, weight]) annotation

[leouk]

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 I tried a visitor that would go over inv/pre/post etc and attempt to calculate some things. This largely works but can get clumsy/complicated - in fairness I wasn't as familiar with the LeafVisitors then.

For instance, the number of conjuncts (i.e. the number of proof goals that a specification part would entail) or disjuncts (i.e. the amount of assumption case analysis or consequence choices) to help identify the proof strategies needed when translating to Isabelle's proof scripts with ps2isa plugin.

Also, if the user "knew" about the complexity of certain constructs (e.g. iota, exists1 versus >=, + etc) in expressions, a (user-defined) weight could be given to the specification. This would then again help the proof strategy inference tool to know whether to try specific assisting tools (e.g., Pressburger or linear arithmetic decision procedures for >=, +, etc.) or not, or to suggest lemmas for the "heavier" operators/parts.

Can also be useful to "count" the specification "semantic" size (as opposed to the nominal LOC size).

What do you think? Is this (at least in the "simple" form of counting spec parts) doable in a reasonably simple visitor or am I kidding myself over the complexity of the annotation visitation side?

Best,
Leo

[nickbattle]

Yes, I think something like that would be possible in a single visitor, though you would have to keep state within the class (which is unusual for a visitor, and means they're "one shot"). Or it may turn out to be easiest with a couple of visitors, with the main one spawning simpler (stateless) "counting" visitors for sub-expressions and the main one collating all the results.