System and method for dynamically inferring data preconditions over predicates by tree learning

1. A method for inferring preconditions for procedures in a program, comprising:

formulating predicates based on inputs to a procedure, including formal arguments, global variables and external environment;

sampling truth assignments to the predicates to provide truth assignments that lead to a feasible set of input values;

generating test cases for testing the program in accordance with the truth assignments having feasible sets of input values; and

classifying the truth assignments to the predicates as providing an error or not providing an error;

wherein the sampling includes random sampling of the truth assignments to the predicates, and the random sampling includes employing a randomized satisfiability solver in combination with a theory solver.

2. The method as recited in claim 1 , wherein formulating predicates includes instrumenting the program with variables to track properties of the program during execution.

3. The method as recited in claim 2 , wherein the predicates are derived from instrumented variables and program variables.

4. The method as recited in claim 1 , wherein sampling includes selecting a previously unseen truth assignment to the predicates and determining its satisfiability.

5. The method as recited in claim 1 , further comprising generating a truth table based upon test outcomes.

6. The method as recited in claim 1 , further comprising applying a tree learning method to the test outcomes to infer preconditions on the inputs of the procedure.

7. A computer readable medium comprising a computer readable program, wherein the computer readable program when executed on a computer causes the computer to perform the steps as recited in claim 1 .

8. A method for inferring preconditions for procedures in a program, comprising:

instrumenting a program with variables to track properties of the program to formulate predicates which are derived from the variables and based on inputs to a procedure, including formal arguments, global variables and external environment;

repeatedly sampling truth assignments to the predicates to provide truth assignments that lead to a feasible set of input values obtained by solving a satisfiability problem corresponding to a chosen truth assignment;

generating test cases for testing the program in accordance with the truth assignments having the feasible sets of input values;

classifying the truth assignments to the predicates as providing an error or not providing an error; and

inferring preconditions on the inputs to the procedure based upon classified truth assignments;

wherein sampling includes random sampling of the truth assignments to the predicates and the random sampling includes employing a randomized satisfiability solver in combination with a theory solver.

9. The method as recited in claim 8 , further comprising generating a truth table based upon test outcomes.

10. The method as recited in claim 8 , further comprising applying a tree learning method to the test outcomes to infer the preconditions on the inputs of the procedure.

11. A computer readable medium comprising a computer readable program, wherein the computer readable program when executed on a computer causes the computer to perform the steps as recited in claim 8 .

12. A system implemented on computer readable medium comprising a computer readable program for inferring preconditions for procedures in a program, comprising:

a program instrumenter configured to instrument a program with variables to track properties of the program to formulate predicates which are derived from the variables and based on inputs to a procedure, including formal arguments, global variables and external environment;

a satisfiability solver and theory solver employed in combination to randomly sample truth assignments to the predicates to provide truth assignments that lead to a feasible set of input values;

a test case generator configured to test the program in accordance with the truth assignments having the feasible sets of input values and to classify the truth assignments to the predicates as providing an error or not providing an error; and

a decision tree learning method configured to infer preconditions on the inputs to the procedure based upon classified truth assignments.

13. The system as recited in claim 12 , wherein the satisfiability solver and theory solver include a satisfiability formula which determines satisfiability for satisfiability problems in the program.

14. The system as recited in claim 12 , further comprising a truth table generated based upon test outcomes.

15. The system as recited in claim 12 , wherein the tree learning method includes an iterative dichotomizer.

16. The system as recited in claim 12 , wherein the tree learning method learns a Boolean function that predicts error-free execution.