| 摘要 |
<p>Provided is a device for dynamic verification of an invariant condition, which comprises: a verification timing database for storing a set of a pair of syntax patterns of an invariant condition and a verification timing for giving a position where the invariant condition is to be evaluated; a program input unit for inputting a program to be verified; an invariant condition input unit for inputting the description of the invariant condition to be satisfied by the program to be verified; a syntax element enumeration unit for enumerating a plurality of syntax elements corresponding to a set of slave elements of the invariant condition, from the description of the invariant condition; a verification timing search unit for searching the verification timing database, to thereby determine at least one verification timing corresponding to the syntax pattern of at least one invariant condition matching the plurality of syntax elements; and a program rewriting unit for rewriting the program to be verified so that the invariant condition is evaluated at a position which is given by the at-least one verification timing.</p> |
