Improve Test Suite

[rcosta358]

The test suite could be improved in several ways to make failures easier to understand and tests easier to maintain.

1. More Informative Failures

Currently, tests only indicate whether they passed or failed. When a test fails, the output should clearly show what went wrong, including the expected result and the actual result. This would make debugging failing tests significantly easier.

2. Inline Error Assertions

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.

3. Multiple Error Assertions

With the change described above, a single test file could contain multiple expected errors, instead of requiring a separate test file for each failure. This would allow the test suite to verify that all expected errors are reported and no unexpected errors occur.

Then, some related tests should be merged into single files, similarly to the tests that should pass.

[cheestree]

Interesting... 👀