Завершение эскизов предикатных программ методом синтеза через контрпримеры

Программа на языке P представляет собой набор определений предикатов. Для языка P разработана операционная семантика. На базе операционной семантики определена формула тотальной корректности предиката относительно его спецификации. Для незаконченной программы на языке P ставится задача её завершения до корректной относительно спецификации. Метод синтеза выражений на основе контрпримеров успешно адаптирован для этой задачи.