| 摘要 |
There is provided a precondition generating apparatus in which a storage stores a set“S”of logical expressions; a creating unit creates a first logical expression being a logical product of the“S”, logical expressions of a program and a negation of a logical expression indicating a postcondition; a solver finds a solution that makes the first logical expression true and specifies a set of clauses that cannot be simultaneously true in the first logical expression if not found; wherein the creating unit sets relaxing variables for the logical expressions belonging to the set“S”in the set of clauses wherein the logical expressions indicates a precondition of the program, generates a second logical expression by alleviating the clauses of logical expressions corresponding to the relaxing variables in the first logical expression, and applies same process as in the first logical expression to the second logical expression. |
