I’m still trying to figure out if some invariant annotations should be inherited from subclass to superclass, i.e. in the opposite direction of regular inheritance and the way annotations are inherited now.
Let’s assume that I do this. @NotThreadWithName is an invariant that makes a precondition stricter, so it will be inherited in the regular way; its behavior is covariant, even though I’m not sure if that’s the right word for it.
@OnlyThreadWithName, I believe, is an invariant that should make the precondition less strict, at least when there are several of them, because my intuition is that users want to combine them using or: It just doesn’t make sense to combine them using and. So let’s assume that I inherit @OnlyThreadWithName from subclass to superclass, i.e. in the opposite direction, or contravariantly.
What does that mean? And does it make sense? Consider the following program with annotations:
class Super {
void foo() { }
void bar() { }
void wibble() { }
}
class Mid extends Super {
@NotThreadWithName("main")
void foo() { }
@OnlyThreadWithName("aux")
void bar() { }
@NotThreadWithName("main")
@OnlyThreadWithName("aux")
void wibble() { }
}
class Sub extends Mid {
void foo() { }
void bar() { }
void wibble() { }
}
Here are the invariants end up getting applied for each method:
Super:foo(): None.fee(): May only be run by threads with name “aux”.wibble(): May only be run by threads with name “aux”.
Mid:foo(): May not be run by threads with name “main”.fee(): May only be run by threads with name “aux”.wibble(): May not be run by threads with name “main”. May only be run by threads with name “aux”.
Sub:foo(): May not be run by threads with name “main”.fee(): None.wibble(): May not be run by threads with name “main”.
The biggest question here is probably how the invariants for Mid.wibble() should be combined. If they are combined using and, then the only thread allowed to run has the name “aux” (not “main” and “aux”); if they are combined using or, then all thread names except for “main” are allowed (not “main” or “aux”). If the names “main” and “aux” are changed so that they are identical, then the possible results are even more nonsensical: No threads at all, or all threads allowed.
I think my intuition about combining annotations that relax the invariants using or was wrong. It should always be and. If a programmer wants to use or, that can be achieved with a little bit more code using a @Combine-style annotation.
Perhaps another idea to investigate would be that of allowing necessary and sufficient predicates: A necessary predicate must be fulfilled for a method to be executed without warnings, but it is not enough by itself; if another predicate fails, a warning is generated. On the other hand, when a sufficient predicate is fulfilled, other predicates may fail, and still no warning is generated. That is a similar notion than combining using and and or, but perhaps more precise. Right now, I don’t see a need for this, though.
The covariant and contravariant inheritance of annotations could be interesting and I have a better idea of how to implement it, but without a connection to the idea of restricting or relaxing preconditions, I don’t quite see a consistent, compelling theory developing. The custom predicates make the theory a little bit wobbly anyway. Also, right now I can’t come up with a situation in software engineering that would require contravariant propagation of annotations.
So, right now it seems like I’ll just add subtyping warnings for predicate annotations, and I noticed I have to do XML import for predicate annotations, and that’s it.
