Right now I’m actually doubting that data annotations are necessary. It seems like assertions can do enough already. For method annotations, the important distinction was that the invariants in the annotations get inherited into subclasses.
The original idea of data annotations was that invariants would be checked every time an object is accessed. However, if I implement the scopes as discussed in the last post, then what’s the difference to assertions? You could simply place several assert
statements in the code. Maybe the annotations would look cleaner, less littered, but is that really a justification for developing data annotations?
Originally, what intrigued me was calling a predicate method every time an object is accessed. In that predicate method, I could do whatever I wanted to do: This even includes implementing a lock-set algorithm and performing dynamic race condition detection.
But the scoping destroys that possibility, because the invariants would not be checked everywhere. So I think the scope idea is not the right way to go. Too bad, I already wrote a generified RangeMap
that I would have used to store invariants that are active in a range of PC (program counter) values…
Maybe the right way to think about data annotations is that you specify the invariant at the time the object is created. Or maybe it’s class-based and you specify the properties inside the class, and then it applies to every instance. Maybe there are multiple places where you can specify invariants, e.g. when you define a field and when you define a parameter. But what invariants are checked when that field is passed as argument for that annotated parameter? Now the limited scope makes sense again. Or is everything merged?
I’ll have to think about this some more…
Update
Maybe it makes sense to have both scoped and unlimited invariants. The scoped invariants would pretty much replace assert
statements littered in one particular area, while the unlimited invariants would follow an object throughout its entire lifetime.
One thing I’ve definitely realized is that the kind of opcode that is about to be executed should be transferred to the predicate method. That way, a predicate method could tell that it’s just before a monitorenter
, for example.