The problem of the automatic discovery of invariant polynomial equalities in program control points is considered. The class of programs with data algebras that are infinite fields is studied in the paper. The results obtained here may also be extended to infinite commutative integral domains. To solve the problem the approximation method is proposed. Four main problems connected with this method are formulated and proved to be decidable.
展开▼
