Изобретение относится к способу верификации программного обеспечения. Технический результат заключается в автоматизации верификации программного обеспечения. В способе семантические правила для создания узлов абстрактного синтаксического дерева синтаксически управляемого определения, исходя из размерной однородности физических уравнений, реализованных в выражениях исходного кода программы, дополняют полем для операции с естественной семантикой идентификаторов, представленной в виде размерности физической величины, интерпретируемой в идентификаторе и описанной одномерным целочисленным массивом, хранящимся в таблице символов, инициализируемой значениями естественной семантики идентификаторов после проведения лексического и синтаксического анализов, при этом указанное поле заполняется автоматически в зависимости от операции с идентификаторами в данном узле, при выполнении восходящего обхода модифицированного абстрактного синтаксического дерева вычисляют значения естественной семантики во внутренних узлах и контролируют выполнение условий корректности выражений исходного кода программы, исходя из значений естественной семантики идентификаторов в таблице символов. 4 ил.
