Введение. Development of effective programs for the standard functions floor, isqrt, and ilog2 under predicate programming technology

Novosibirsk 2010

V.I. Shelekhov

Development of effective programs for the standard functions floor, isqrt, and ilog2 under predicate programming technology

Preprint
154

Development of effective programs for the standard functions under predicate programming technology is described. The developed functions are integer part of float value, integer square root, and integer part of binary logarithm.

© A. P. Ershov Institute of Informatics Systems, 2010

Проведен эксперимент по разработке нескольких небольших программ на C++ по технологии предикатного программирования [5] с формальной верификацией в системе автоматического доказательства PVS [1]. Среди них ¾ быстрые программы вычисления стандартных функций: целой части плавающего числа, целочисленного квадратного корня и целочисленного двоичного логарифма. Опыт разработки и верификации этих трех программ описывается в данном препринте. Программы указанных стандартных функций используются в программной части известной системы спутниковой навигации «Навител Навигатор» для автомобилей; их исходные коды на C++ приведены в приложениях 2 - 4. Была поставлена задача по возможности ускорить программы данных функций и проверить их правильность посредством формальной верификации на PVS, используя ранее разработанный алгоритм генерации условий корректности предикатных программ с однозначной спецификацией [2, 3].

Последовательность работ, проводимых для каждой стандартной функции, следующая. На основе исходного кода стандартной функции (см. приложения 2 - 4) с использованием описаний алгоритмов, размещенных в Интернете, воспроизводилось математическое описание алгоритма, использованное для программирования данной стандартной функции. На базе математического описания алгоритма строилась соответствующая предикатная программа. Далее проводилась оптимизирующая трансформация [5] предикатной программы с получением программы на императивном расширении языка предикатного программирования P [4]. Наконец, программа конвертировалась с императивного расширения на язык С++. Целью описанного процесса является построение такой предикатной программы и такой последовательности трансформаций, чтобы в результате получить исходный код стандартной функции. Когда эта цель достигалась, к предикатной программе применялся алгоритм генерации условий корректности программы с построением набора теорий на языке спецификаций PVS. Далее проводился процесс доказательства на PVS сгенерированного набора лемм. Для каждой из трех стандартных функций этот процесс был длительным и трудоемким и сопровождался доказательством серии дополнительных математических свойств с построением дополнительных теорий и библиотек теорий на PVS. Отметим, что генерация условий корректности и оптимизирующие трансформации проводились вручную.

Пусть предикатная программа представлена оператором S со спецификацией в виде тройки Хоара:

pre P(x) { S } post Q(x, y)

Здесь x ¾ список аргументов, y ¾ список результатов оператора S,
P(x) – предусловие, Q(x, y) ¾ постусловие оператора. Спецификация является тотальной (реализуемой) и однозначной, если истинна формула:

"x. P(x) Þ $! y. Q(x, y).

Здесь x ¾ аргументы, а y ¾ результаты оператора. Доказательство тотальной корректности для однозначных программ с тотальной (реализуемой) спецификацией можно проводить по более простой формуле [3]:

P(x) & Q(x, y) Þ LS(S)(x, y), (1)

где LS(S) ¾ предикат, являющийся логическим эквивалентом оператора S в соответствии с логической семантикой [2]. Имеется алгоритм генерации условий корректности, эффективно декомпозирующий приведенную формулу в набор удобных для доказательства условий корректности в зависимости от структуры оператора S. Правила этого алгоритма, используемые в данном препринте, приведены в приложении 1.

Эффективная императивная программа на императивном расширении языка P [4] получается применением последовательности трансформаций предикатной программы [5]. Базовыми трансформациями являются:

– склеивание переменных, реализующее замену нескольких переменных одной;

– замена хвостовой рекурсии циклом;

– подстановка определения предиката на место его вызова;

– кодирование структурных объектов низкоуровневыми структурами с использованием массивов и указателей;

– развертка цикла.

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

Дата добавления: 2015-06-27