Automatically exported from code.google.com/p/korattester
This is an Eclipse plugin that implements the Korat algorithm to generate test candidates for Java programs. Korat is 'a novel framework for automated testing of Java programs. Given a formal specification for a method, Korat uses the method precondition to automatically generate all (nonisomorphic) test cases up to a given small size. Korat then executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output.'
From 'Korat: Automated Testing Based on Java Predicates' by Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov
This can be automated with JUnit.