| 摘要 |
<p>PROBLEM TO BE SOLVED: To efficiently obtain program specification.SOLUTION: In a program specification estimation device as one embodiment of the present invention, a predicate generation unit generates a plurality of negation cover sets, each comprising a plurality of predicates including a parameter, in which a conjunction of discretionary 0 or more predicates negates a conjunction of other predicates, a first contradictory nucleus enumeration unit enumerates first contradictory nucleuses on the basis of all predicates included in the plurality of negation cover sets, a program conversion unit converts the program into the form of a logical expression and acquires a program logical expression, a second contradictory nucleus enumeration unit sets slack variables, each assuming a true or a false value, for all of the predicates included in the plurality of negation cover sets, finds a solution that makes true a logical expression including a disjunction with each of the slack variables and a predicate corresponding to each of the slack variables, the program logical expression, and a conjunction with additional constraint so as to satisfy a constraint, etc., that at least one of the predicates included in each of the first contradictory nucleuses holds true and the rest is false, and converts a correction set that is a set of predicates in which the slack variable holds true, into the contradictory nucleus.</p> |
