JUnit

Installation instructions JUnit, and links to further information, can be found here.

TestNG

TestNG is a framework similar to JUnit and is claimed to overcome some of the limitation of JUnit. More information here. TestNG is used by the tool jmlunitng presented in this course.

JML tool kit

This year we include for the first time a 'new' tool for JML parsing, called OpenJML. Instructions for this tool can be found here.

Older versions of JML parsing tools can be found here, in case you run in to troubles with OpenJML.

• Lab 2 on formal specification to check the syntax of your specifications
• Using JMLUnitNG to automate test case generation.

Please read there instructions carefully. If you still experience problems, post them to our Google group. This way, you can help each other. And finally, you may also contact the course assistants.

JMLUnitNG

A black box testing tool that relies on a jml checker and the TestNG tool. It will be introduced in the lectures/exercises on black box automated test case generation. JMLUnitNG homepage

KeY Test Generation

• You can download the Eclipse plugin for test case generation. Within Eclipse, click on Help|Install New Software...
  A window will open. In the textfield with label "Work with:" insert the address

  http://www.cse.chalmers.se/~gabpag/eclipse/

  The middle area will be filled with a checkbox. Check it and press Next. Accept everything it comes later (or if you are paranoid, read what it says before deciding whether to accept) Restart Eclipse as it tells you to do. KeyTestGen is installed.
  
  
• An older version of the generator is available as a JNLP file for Java Webstart. Simply say

  javaws http://www.key-project.org/download/testingTDV/KeYTest.jnlp

KeY-Hoare System

Can be downloaded here. A paper explaining the system including a brief reference manual is here.