*Result*: TestEra: A Novel Framework for Testing Java Programs
*Further Information*
*TestEra is a novel framework for automated specification-based testing of Java programs. Given a formal specification for a method, TestEra uses the method precondition to automatically generate all nonisomorphic test inputs up to a given bound. TestEra executes the method on each test input, and uses the method postcondition as a test oracle to check the correctness of each output. TestEra allows users to give specifications as first-order logic formulae. As an enabling technology, TestEra uses the Alloy toolset, which provides an automatic tool for analyzing first-order logic formulae. We have used TestEra to check several Java programs including a networking architecture, the Alloy-alpha analyzer, and methods from the Java Collection Framework. This article describes the TestEra framework and gives experimental results.*