Sketch completion for predicate programs by counterexamples guided synthesis.pdf 1. Система предикатного программирования Программа на языке P0 определяется следующей конструкцией: (:){}, аргументы и результаты - непересекающиеся наборы имён переменных. Набор аргументов может быть пустым. Операторами языка P0 являются: B(x : z); C(z : y) -последовательный оператор; B(x : y)||C(x : z) -параллельный оператор и if (e) B(x : y) else C(x : y) -условный оператор. Здесь B и C - операторы, e - логическое выражение [1]. Операционной семантикой программы H(x : y) назовём формулу R(H)(x,y), смысл которой на естественном языке звучит следующим образом: «для значения набора x исполнение программы H всегда завершается и существует исполнение, при котором результатом вычисления является значение набора y» [2]. Тотальная корректность программы относительно спецификации в виде предусловия P(x) и постусловия Q(x,y) определяется формулой Vx P(x) ^ [Vy R(H)(x,y) ^ Q(x,y)] & 3y R(H)(x,y). В системе предикатного программирования реализован генератор формул корректности. Используя систему правил вывода, генератор декомпозирует исходное условие тотальной корректности на более простые формулы корректности, которые проходят проверку в SMT-решателе CVC3 и в системе PVS [3]. 2. Завершение эскизов предикатных программ Синтаксис выражений языка P расширяется произвольным выражением, для обозначения которого используется слово «??». Программа, содержащая в себе произвольные выражения, называется эскизом [4]. Примеры программ на языке P, формул корректности и эскизов можно найти по ссылке [5]. Пусть дан некоторый эскиз Sketch(x : y), произвольные выражения которого заменены на вызовы предикатов f,, тела которых неизвестны. Этот эскиз передаётся генератору формул корректности, который строит множество формул корректности. Для некоторой пары значений (x',y') эскиза Sketch(x : y) строится конкретный пример [6] каждого произвольного выражения по следующему алгоритму. Значения (x', y') подставляются в множество формул корректности. Формулы в полученном множестве зависят лишь от значений произвольных выражений, которые можно найти, передав формулы в SMT-решатель. Значения выражений объединяются с парой (x',y'), образуя конкретные примеры произвольных выражений. Спецификация [P(x), Q(x, y)] эскиза Sketch(x : y) приводится к виду P(x) ЛQ(x, y) и передаётся SMT-решателю; он находит значения переменных (x0,y0), на которых эта формула истинна. Для каждого произвольного выражения строится множество конкретных примеров, начальным элементом которого является конкретный пример для пары значений (x0,y0). Для каждого множества конкретных примеров строится удовлетворяющее ему выражение по следующему алгоритму. Выражения языка P сортируются в порядке возрастания их длины и поочередно проходят проверку на удовлетворение конкретным примерам. Если выражение удовлетворяет всем конкретным примерам заданного множества, то оно считается итоговым. Построенные таким образом выражения подставляются в множество условий корректности эскиза Sketch(x : y). Полученное множество формул передается SMT-решателю. Если решатель подтверждает истинность формул, то процесс синтеза завершается. Если SMT-решатель смог найти контрпример (x'',y''), на котором не все формулы корректности истинны, то для этого контрпримера строятся конкретные примеры произвольных выражений, расширяющие существующие множества конкретных примеров. Процесс повторяется для обновлённых множеств. 3. Оценка сложности метода Сложность алгоритма зависит от количества формул в множестве условий корректности, от количества кандидатов на роль выражения, удовлетворяющего множеству конкретных примеров, и от возможностей решателя. Зависимость количества формул корректности от объёма программы экспоненциальная. В среднем для программы объёмом в 10 операторов сгенерируется 30 формул корректности. Зависимость числа возможных кандидатов на роль выражения, удовлетворяющего множеству конкретных примеров, от длины выражения экспоненциальная. В среднем выражение длиной 10 лексем имеет 100 тыс. кандидатов. В данной реализации используется решатель CVC3. Он корректно завершает проверку выполнимости лишь для простых формул, не содержащих кванторов и сложной арифметики. Таким образом, описанный выше алгоритм целесообразно применять для коротких простых программ.

Скачать электронную версию публикации