Patent ID: 8707273

Claim:
A precondition generating apparatus comprising: a symbolic execution unit configured to perform symbolic execution on a program described by an imperative programming language to obtain a program logical expression; a first storage configured to store a set “S” of a plurality of logical expressions “A”s, the logical expressions “A”s being described using variables included in the program; a second storage configured to store a logical expression “B” that is described using variables included in the program, the logical expression “B” indicating a postcondition of the program; a logical expression creating unit configured to create a first logical expression that is a logical product of the logical expressions “A”, the program logical expression and a negation of the logical expression “B”; a problem solver configured to find a solution that makes the first logical expression true and if the solution does not exist, specify a set of clauses that cannot be simultaneously true in the first logical expression; a third storage configured to store a set of all of logical expressions “A”s included in the set of the clauses as indicating a first precondition of the program; and a fourth storage configured to store the set of all of the logical expressions “A”s as a relaxed clause set “N 1 ”, wherein the logical expression creating unit (A1) sets relaxing variables having values of true or false for the logical expressions “A”s belonging to the relaxed clause set “N 1 ”, (B1) acquires a set “NN 1 ” that is a set of logical expressions being logical sums between the logical expressions “A”s belonging to the relaxed clause set “N 1 ” and the relaxing variables, (C1) if a number of the logical expressions “A”s belonging to the relaxed clause set “N 1 ” is two or more, acquires a logical sum of negations of the relaxing variables as a variable selection clause “v 1 ”, and (D1) generates a second logical expression that is a logical product following items: (a) logical expressions belonging to a set “S−N 1 ” that the relaxed clause set “N 1 ” is subtracted from the set “S”, (b) logical expressions belonging to the set “NN 1 ”, (c) the variable selection clause “v 1 ”, (d) the program logical expression, and (e) a negation of the logical expression “B”, the problem solver finds a solution that makes the second logical expression true and if the solution does not exist, specifies a set of clauses that cannot be simultaneously true in the second logical expression and the third storage stores a set of all of logical expressions “A”s included in the set of the clauses specified for the second logical expression as indicating a second precondition of the program.