Модели программ

Для решения задач автоматической генерации программных инвариантов в качестве модели программ используются U-Y схемы программ над памятью, интер­пре­ти­рован­ные над алгебрами данных. В этой модели программу представляет инициальный ориентированный граф с выделенными заключительными вершинами. Вершины этого графа называются состояниями, а дуги – переходами. Состояния программы – суть ее контрольные точки. Переходы программы отмечены условиями и вычисляющими операторами (определения см. ниже). Эта модель по существу эквивалентна модели transition system, используемой в современных работах западных авторов. Отметим, что эта модель представляет неструкту­ри­ро­ван­ную программу.

Наши алгоритмы доказательства и генерации полиномиальных инвариантных равенств для программ, алгеброй данных которых является поле или области целостности. в качестве модели программы используют выражения в алгоритмической алгебре Глушкова, представляющие структурированные программы.

Различие моделей программ не является существенным, т.к. для преобразования U-Y схемы программы в эквивалентное ей выражение алгоритмической алгебры Глушкова можно использовать, например, алгоритм анализа конечного автомата.

Алгоритм вычисле­ния полиномиальных инвариантных равенств, изложенный ниже, основан на свойстве нетеровости колец полиномов. Мы рассмотрим предложены алгоритмы, основанные на вычислениях базисов Гребнера.

Основные операции алгоритмической алгебры Глушкова:

, (1)

Здесь P, Q – программы, а u – условия. Семантику этих операций определим с помощью операторов языка Паскаль:

~ // последовательное выполнение

~ If u then P else Q

~ While u do P