Test Case Generation with KeY

KeY is usable as a white-box-testing tool. This means that KeY can create JUnit test cases from proofs (or proof attempts) based on the information obtainable from the proof tree. Since a proof tree in KeY is basically a symbolic execution tree it can provide valuable information such as execution path conditions and thus facilitates a high code coverage of the created tests.

KeY can be started in a test generation optimized mode using the command line parameter unit (runProver unit). After a proof tree has been produced test cases are created by clicking the menu item Tools->Create Unittests .

Users that are solely interested in automatic test case generation can also start KeY in a mode that hides features irrelevant for testing. This is triggered by the command line parameter testing: