Введение. Верификация и синтез эффективных программ стандартных функций в технологии предикатного программирования

Верификация и синтез эффективных программ стандартных функций в технологии предикатного программирования

В.И. Шелехов

Код функции ilog2 из файла fast_log2.cpp

Код функции floor из файла fast_floor.cpp

int32_t os::fast_floor(float _f) {

uint32_t dw = reinterpret_cast<uint32_t &> (_f);

if (int32_t(dw) < 0) {

//

// For negative values.

//

dw &= 0x7FFFFFFF;

if (dw == 0)

return 0;

const int32_t sh = 23 + 127 - (dw >> 23);

if (sh >= 24)

return -1;

else if (sh < 0) {

// NOTE: precision is lost.

return -int32_t((0x00800000 | (dw & 0x007FFFFF)) << (-sh));

} else {

if (dw & (0x007FFFFF >> (23 - sh)))

// NOTE: the number has fractional part.

return -int32_t((0x00800000 | (dw & 0x007FFFFF)) >> sh) - 1;

else

// NOTE: the number is whole.

return -int32_t((0x00800000 | (dw & 0x007FFFFF)) >> sh);

}

} else {

//

// For positive values.

//

if (dw == 0)

return 0;

const int32_t sh = 23 + 127 - (dw >> 23);

if (sh >= 24)

return 0;

else if (sh < 0)

// NOTE: the precision is lost.

return (0x00800000 | (dw & 0x007FFFFF)) << (-sh);

else

return (0x00800000 | (dw & 0x007FFFFF)) >> sh;

}

}

Приложение 4

uint32_t os::fast_log2(uint32_t _dw) {

uint32_t log2 = 0;

while (_dw!= 0) {

++log2;

_dw >>= 1;

}

return log2;

}

Разработка эффективных программ стандартных функций floor, isqrt и ilog2 по технологии предикатного программирования

Препринт
154

Рукопись поступила в редакцию 25.04.10

Редактор Т. М. Бульонкова

Рецензент И.С. Ануреев

Подписано в печать 10.06.10

Формат бумаги 60 ´ 84 1/16 Объем 2.6 уч.-изд.л., 2.8 п.л.

Тираж 60 экз.

Центр оперативной печати «Оригинал 2»
г.Бердск, ул. О. Кошевого, 6, оф. 2, тел. [phone]

Описывается технология построения эффективных программ стандартных функций isqrt, floor и, ilog2. Корректность программ обеспечивается дедуктивной верификацией и программным синтезом. Условия корректности программ доказываются с помощью системы автоматического доказательства PVS.

Ключевые слова: предикатное программирование, дедуктивная верификация, программный синтез, тотальная корректность программы

Формальная верификация занимает особое место среди других методов верификации программ: она обеспечивает стопроцентную гарантию правильности программы относительно ее спецификации, что недостижимо применением самых совершенных методов тестирования программ. Формальная верификация подразделяется на дедуктивную верификацию и проверку на модели (model checking).

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

Дедуктивная верификация гарантирует корректность программы относительно ее спецификации доказательством истинности формул корректности программы. Доказательство проводится с помощью некоторой системы автоматического доказательства. Формулы корректности программы генерируются автоматически по формулам логики и спецификации программы путем применения системы логических правил. Формулы логики программы извлекаются из неё с помощью формальной (денотационной, операционной, аксиоматической,...) семантики языка программирования. Для современных императивных языков чрезвычайно трудно построить формальную семантику. Однако для языка C формальная семантика разработана [17, 18]. Проведение дедуктивной верификации реальных программ требует больших затрат времени и высокой квалификации коллектива инженеров-верификаторов[1]. Как следствие, применение дедуктивной верификации экономически оправдано лишь для программ с высокой ценой ошибки.

Программный синтез реализует логический вывод программы из ее спецификации в рамках некоторой системы автоматического доказательства. Полученная в результате синтеза программа является корректной по построению. По своей силе программный синтез приравнивается к формальной верификации.

Метод разработки программы на базе модели предполагает построение абстрактной модели программы. Корректность модели обеспечивается проведением валидации и верификации. Код программы генерируется из модели в автоматизированном режиме или в автоматическом.

Перечисленные методы формальной верификации, программного синтеза и разработки программы на базе модели относятся к классу формальных методов, применяемых при спецификации, разработке и верификации программ.

Несмотря на серьезные трудности применения существующих методов дедуктивной верификации, на настоящее время в мире существует более сотни[2] проектов дедуктивной верификации реальных производственных программных систем. Большие коллективы инженеров-верификаторов, крупные исследовательские центры по автоматическому доказательству и формальной верификации, специальные фонды и государственная поддержка ¾ все это имеется в США, Англии, Франции, Германии Австралии и других странах.

До сих пор дедуктивная верификация и автоматическое доказательство теорем считаются в России бесперспективными направлениями исследований, тогда как в США, Германии и Англии эти направления интенсивно развиваются начиная с 1980-х годов. Указанные направления не входят в список критических технологий и отсутствуют в перспективных планах Российской академии наук.

Между тем, неумолимо приближается время, когда применение формальной верификации станет обязательным требованием сертификации жизненно важных программ. Ведущие банки США и Европы уже лет пять назад установили это требование для сертификации банковских программ, работающих с пластиковыми картами клиентов. Космическое агенство NASA применяет дедуктивную верификацию при разработке программ уже более 15 лет, а компании Боинг и Аэробас – почти 10 лет. В последней версии международного стандарта DO-178C для бортовых программ самолетов узаконено применение формальных методов и уточнены условия их использования при сертификации программ [12, 13]. На очереди принятие аналогичных стандартов для программ, используемых в энергетике, медицине и других областях. Впечатляют достижения компании Microsoft, которой удалось провести дедуктивную верификацию сложнейшей компоненты операционной системы Windows размером 300 тыс. строк на языке C [14].

Методы программного синтеза и дедуктивной верификации описываются в настоящей статье на примерах разработки быстрых программ для стандартных функций: floor – целой части плавающего числа, представленного в бинарном формате в соответствии со стандартом IEEE 754-2008; isqrt – целочисленного квадратного корня и ilog2 – целочисленного двоичного логарифма. Программы указанных стандартных функций на языке C++ используются в известной отечественной системе спутниковой навигации “Навител Навигатор” для автомобилей.

Дедуктивная верификация и синтез предикатных программ определяются в разделе 1. Предлагаемые методы верификации и синтеза базируются на концепции логической семантики и принципиально отличаются от классических методов Флойда и Хоара [15, 16]. Синтез программ целочисленного квадратного корня и целой части плавающего числа описывается в разделах 2 и 3. Формулы корректности программ стандартных функций были доказаны с помощью известной системы автоматического доказательства PVS [4]. Обзор смежных работ представлен в разделе 4. Опыт разработки программ указанных стандартных функций в режимах верификации и синтеза суммируется в разделе 5.

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