Invariant condition generating device, computer program, invariant condition generating method, program code manufacturing method

摘要

PROBLEM TO BE SOLVED: To provide a novel technique for generating invariants.SOLUTION: An invariant generator 100 includes a storage unit 300 having a program code stored therein, and a processing unit 200 for executing invariant generation processing. The processing unit 200 executes a third process for generating an invariant. The third process includes; a matrix generation process for generating a representation matrix, which is a transpose of a transformation matrix representing transformation of each of one or more sub-expressions made by execution of a program code; an arithmetic process for deriving an eigenvalue and eigenvector of the representation matrix; and an invariant generation process for generating an invariant based on a set of eigenvalue and eigenvector and the one or more sub-expressions.SELECTED DRAWING: Figure 1