The tests only verify whether the expected type of error is correct (RefinementError, SyntaxError, etc.). This could be improved by also validating:

• The exact line where the error should be reported
• The error title the error should have
• The error message the error should have

To this end, instead of declaring the expected error titles at the beginning of the file or in a separate .expected file, they could be written directly on the line where it should occur, along with its title and message.

Example:

void test() {
    @Refinement("x > 0")
    int x = -1; // Refinement Error: #x_1 == -1 is not a subtype of #x_1 > 0
}

However, it is unclear whether instance variable identifiers may change between executions. If they are not deterministic, performing an exact comparison of the full error message should not be done. In that case, we may need to reconsider how message comparisons should be done.