| 主权项 |
1. A program specification estimation device, comprising:
first circuitry to analyze a program described by an imperative programming language and detect a parameter included therein, and generate a plurality of negative covering sets each of which includes a plurality of predicates each including the parameter wherein a conjunction of arbitrary zero or more predicates in each negative covering set is a negation of a conjunction of the other predicates therein; second circuitry to list first unsatisfiable cores that are minimal sets of the predicates that respective conjunctions thereof conflict, on a basis of all the predicates included in the plurality of negative covering sets; third circuitry to convert the program to a form of a logical formula with use of symbolic execution to obtain a program logical formula; and fourth circuitry to (A) set a relaxing variable which takes a true or false value to each of all the predicates included in the plurality of negative covering sets, (B) obtain a solution that makes a logical formula be true so as to satisfy a first constraint and a second constraint, the logical formula including a conjunction of (1) a disjunction of each of the relaxing variable and the predicate corresponding to each of the relaxing variable, (2) the program logical formula and (3) an additional constraint given beforehand, the first constraint being a constraint related to a number of relaxing variables to be true, that is determined according to a number of the negative covering sets generated by the first circuitry, and the second constraint being a constraint that at least one of the predicates included in each of the first unsatisfiable cores becomes true and the rest of the predicates become false, and (C) convert a correction subset that is a set of the predicates for which the relaxing variables have become true to a second unsatisfiable core, the second unsatisfiable core being a minimal set of the predicates which cannot be made true simultaneously with the additional constraint in a case of finding a solution that makes a logical formula including a conjunction of (1) the second unsatisfiable core, (2) the program logical formula and (3) the additional constraint be true. |
