Work proposal: add corpus of tests for SANY at syntax parsing level

[ahelwer]

Work proposal: add corpus of tests for SANY at syntax parsing level

[kape1395]

I like this idea. The "DSL" sounds similar to the TLAPM tests, e.g. https://github.com/tlaplus/tlapm/blob/main/test/fast/basic/z3_false_test.tla. Here, the file contains relevant theorems, and the expected result is stated after the module. The part after the module is ignored by parsers, so the module itself is valid as is. The expectation definition has to be more elaborated in the case of the parser, compared to the proof tests.

[lemmy]

The more tests the better, although almost all TLC tests implicitly test SANY; its test coverage should not be too bad.

More importantly, will these tests be independent of the existing test suite unless we upgrade to junit5? I see value in having a single, uniform test suite. If this is the case, we should explore upgrading to junit5 first.

[ahelwer]

These tests will be added alongside the current test suite. It will just be a single junit test that runs the entire test corpus, and fails if any of them fail. The only real benefit to using dynamic tests in junit 5 is it should make each corpus test appear as a single individual unit test; you can see it in this video, it looks quite nice in the eclipse UI: https://www.youtube.com/watch?v=8kxgO0Fv6d4

I agree SANY gets exercised a lot with the existing test suite, but I don't think existing tests are sufficient to confidently modify SANY itself if we want to do that (I do want to do that lol).

[lemmy]

To evolve SANY, we not only require blackbox tests but also whitebox tests that access and validate SANY's internal state during testing - SANY is more than a parser. It's fine if these blackbox tests cannot access SANY programmatically, but we want seamless integration with the existing and future whitebox tests. If JUnit4 doesn't have the necessary features, upgrading to JUnit5 seems like a sensible first step.

That said, I would like to point out that the fine-grained "debuggability" of the current test suite is worth the effort of writing what some call verbose/cumbersome tests for the existing test suite; it's a price paid only once. Moreover, I presume that Java's preformatted strings will make writing new tests a lot more convenient.

[ahelwer]

Sure, I would like to have several levels of tests - syntax parsing being the lowest, unless the lexer can be accessed independently - then adding on semantic tests and finally level tests.