Because of the difficulty of writing formal specifications, formal methods are considered expensive and often only used in so called safety-critical systems. Broader acceptance might be possible if tools provide assistance in handling formal methods. We present a framework, developed by Johannes Henkel and Amer Diwan at Colorado University, that, given a Java Class, suggests an algebraic specification of that class by considering observable equivalences of objects. Furthermore their framework allows to execute an algebraic specification, providing a proto type that can be used by clients, or to check an implementation of a Java class against its specification.