Patent ID: 7844951

Claim:
A computerized method of generating a specification from an implementation, the method comprising: receiving an implementation comprising a modifier method and an observer method of a class implementing an abstract data type, wherein the modifier method is configured to modify state of an object instance of the class and the observer method is configured to return the state of the object instance of the class; symbolically executing the modifier method to obtain constrained states of the modifier method by at least performing computations on symbolic values of the modifier method to accumulate path conditions for execution paths of the modifier method; wherein the obtained constrained states are created based on final states of the execution paths and the final states projected onto initial state of the execution paths; applying the observer method in the obtained constrained states to obtain specialized axioms for the execution paths of the modifier method; and creating a specification of the modifier method from the obtained specialized axioms based on generalizing, merging and simplifying the specialized axioms, wherein the specification comprises a parameterized unit test comprising input parameters, program statements, and one or more assertions verifying the behavior of the modifier method.