2017 г., Том 22, Специальный выпуск, с.44-59

При разработке в ИСИ СО РАН дедуктивной системы C-light встала задача создания специализированных версий генераторов условий корректности (УК). Для ее решения использована концепция метагенерации УК.

Концепция семантических меток позволяет использовать саму процедуру генерации УК для построения их объяснений. Система C-light простым образом дополняется таким расширением с помощью метода метагенерации.

Проблема элиминации инвариантов циклов является алгоритмически разрешимой для циклов специального вида с помощью символического метода верификации финитных итераций. Для таких циклов применяются специальные правила вывода, позволяющие отказаться от использования инварианта цикла. Метод метагенерации позволил удобным образом расширить систему C-light такими правилами.