TestEra is a framework for specification-based testing of Java programs. To test a Java method, TestEra uses the method’s pre-condition specification to generate test inputs and the post-condition to check correctness of outputs.
Examples on Alloy model generation, Alloy input generation and visualization, and JUnit test generation are provided in package edu.utexas.testera.examples.