JMLTests

JMLTests

JMLTests is a new subproject of jmlspecs devoted to creating a common testing framework that can be used by the developers of a variety of JML-based tools. Our goal is to use the large library of tests developed for the JML2 project. Those tests are tightly coupled to the JML2 tools and Makefiles. With JMLTests we plan to introduce a layer of abstraction so that developers of individual JML-based tools can adapt the tests to their needs while maintaining a single common test corpus.

We are currently gathering requirements for JMLTests.

Some preliminary thoughts on the design of JMLTests are also posted.