@Model annotation
John Tang Boyland
with Java annotations, there are two possibilities: (1) provide fields
and methods that describe the operation in Java and (2) describe the
invariants as strings.
In either case, an optional mechanism could be used to check the
invariant. The disadvantage of (2) is that the tool will need to
parse/type-check the strings in order to do its work, and refactorings
of the code will need to be followed by hand refactorings of the
strings. The disadvantage of option (1) is that the extra fields and
methods negatively impact the performance of the code. I have been
told that engineers are unwilling to use annotation processors if they
lead to larger code size, longer (JIT) compilation times and larger
objects (excess fields).
Thus I propose a @Model annotation that could be attached to any Java
element that indicates that the annotated object should be omitted
from the runtime image. This will permit option (1) to avoid the
efficiency problem described above.
Statically, the Java compiler could ensure that methods NOT annotated
@Model could not refer to names annotated @Model. @Model would have
classfile retention.
If desired, one could even have @Model local variables in non-model
methods, but then the checking rules would have to be smarter in that
model locals could not be used in statements that directly affect non-
model variables. (Indirect effects or side-effects would be permitted
by default, but would be frowned upon, as they are in Java's
assertions.)
John