Contract annotations for Java-FV formal verification (@NotNull, @Pure, @Immutable, @Requires, @Ensures, @Invariant, @Frame, @Throws)