I’ve realized that, in order to maximize code-reuse, I’ll have to change the XML format for the concurrency definition again. In the past, the XML node for the annotation didn’t have any child nodes that described classes or methods; in the proposed format, the classes and methods would be the child nodes. This wouldn’t really be a problem with the example I’ve used so far, but predicate annotations are more complex, and I don’t want to mess with them. It would make it more difficult to implement, so I’m taking the easy way out and proposing the following syntax:
All I’ve done is add the invariant node, which will contain the annotation. That means the three valid child nodes for a <threadcheck:def> node are invariant, class, and method, and there needs to be at least one invariant node and at least one of the other two node types. Very simple.
