We currently use scons scripts as a regression test framework. However, these scripts only support testing that examples are successfully translated, generated, and verified. We don't support testing that an example appropriately fails. It would be useful to have support for checking for proper failures. This would let us, for example, have a regression test that ensures that the compilation checker continues to correctly reject various uncompilable programs.
Dafny uses .expect files to allow this kind of testing. This project should have something similar.
We currently use scons scripts as a regression test framework. However, these scripts only support testing that examples are successfully translated, generated, and verified. We don't support testing that an example appropriately fails. It would be useful to have support for checking for proper failures. This would let us, for example, have a regression test that ensures that the compilation checker continues to correctly reject various uncompilable programs.
Dafny uses .expect files to allow this kind of testing. This project should have something similar.