Код функции isqrt из файла fast_sqrt.cpp

Заключение

Итоги

Программа, находящаяся в файле fast_log2.cpp (приложение 4), соответствует программе ilog2, представленной в разд. 4.1. Имеется различие: fast_log2(0) = 0, тогда как ilog2 не определена для 0. На других сайтах встречались программы, для которых ilog2(0) = 0 под режимом, включаемом по желанию пользователя.

Императивная программа, построенная для ilogB в разд. 4.2, должна быть значительно быстрее, чем fast_log2.cpp. На разных сайтах встречались другие алгоритмы для ilog2. Имеется алгоритм, представленный на сайте

http://www.aggregate.org/MAGIC/

Это более быстрый алгоритм, использующий подпрограмму подсчета числа единиц. Оба эти алгоритма не используют условных операторов и в сумме должны быть быстрее ilogB.

Проведенный эксперимент подтверждает универсальность технологии предикатного программирования, позволяющей воспроизвести любую императивную программу в классе задач дискретной и вычислительной математики. Полученные программы для функций isqrt и floor на императивном расширении языка P близки к соответствующему исходному коду на С++; отличия имеются, но они не являются принципиальными. Полученная программа для функции ilog2 существенно быстрее исходной программы на С++.

Алгоритм генерации условий корректности не претерпел существенных изменений в ходе данного эксперимента. Проведены лишь уточнения для генерации на PVS битовых операций над натуральными. Можно констатировать, что задача генерации условий корректности решена успешно. Генерируемые условия корректности декомпозированы достаточно хорошо. Узким местом является верификация условий корректности на PVS. Доказательство на PVS оказалось нетривиальным и трудоемким процессом. Трудности возникали не столько при доказательстве самих условий корректности, сколько при доказательстве используемых математических свойств.

В процессе верификации обнаружено 5 ошибок. Из них четыре ¾ чисто технические ошибки в предикатных программах или при генерации вручную условий корректности. Принципиальной является ошибка, обнаруженная для функции floor: результат функции floor не помещается в отведенные для него m битов для достаточно большого плавающего числа такого, что E – bias >= m – 2 (или d >= w). Ситуация вроде бы очевидная, однако на практике многие ее не учитывают. Ошибка обнаружена в ходе доказательства условия корректности, сгенерированного PVS для функции flval1: требуется доказать принадлежность результата flval1 типу intm. Обнаруживается, что из-за ошибки доказать такое невозможно. На примере данной ошибки становится очевидным, что формальная верификация является наиболее мощным инструментом в обеспечении надежности программ.

В заключение приведем информацию о времени выполнения различных этапов работ по трем функциям:

Для функции isqrt:

· поиск по Интернету, разработка алгоритма по технологии предикатного программирования – 4 дня;

· верификация – 9 дней, из них 5 дней на доказательно леммы or_eq_plus;

· написание отчета – 3 дня.

Для функции floor:

· поиск по Интернету, изучение стандартов и разработка алгоритма – 5 дней;

· верификация – 8 дней, из них полтора дня на доказательно собственно условий корректности;

· написание отчета - 4 дня.

Для функций ilog2 и ilogB:

· - разработка алгоритмов ilog2 и ilogB: 2 дня;

· - верификация: 6 дней;

· - написание отчета: 2 дня.

Относительно большое время, затраченное на верификацию, отчасти объясняется тем, что автор еще не освоил систему PVS в достаточной степени.

Список литературы

1. PVS Specification and Verification System.. — SRI International. — http://pvs.csl.sri.com/doc/

2. Шелехов В.И. Исчисление вычислимых предикатов. — Новосибирск, 2007. — 24с. — (Препр. / ИСИ СО РАН; N 143).

3. Шелехов В.И. Модель корректности программ на языке исчисления вычислимых предикатов. — Новосибирск, 2007. — 50с. — (Препр. / ИСИ СО РАН; N 145).

4. Шелехов В.И. Язык предикатного программирования P. — Новосибирск, 2002. — 40с. — (Препр. / ИСИ СО РАН; N 101).

5. Шелехов В.И. Введение в предикатное программирование. — Новосибирск, 2002. — 82с. — (Препр. / ИСИ СО РАН; N 100).

Приложение 1

В данном приложении приведены правила, используемые при генерации условий корректности.

Теорема 2.1 тождества спецификации и программы. Рассмотрим программу со спецификацией в виде тройке Хоара:

{P(x)} S(x: y) {Q(x, y)} (2.15)

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

P(x) & Q(x, y) Þ LS(S(x: y)) (2.16)

Тогда программа (2.15) является корректной.

Пусть имеется нерекурсивный вызов предиката A(x: y) со спецификацией:

{P(x)} A(x: y) {Q(x, y)} (3)

Для нерекурсивного вызова предиката A(x: y) определим правило:

Правило FB1. R(x, y) ├ P(x) & Q(x, y)

Лемма 15. Допустим, нерекурсивный вызов предиката A(x: y) является корректным, а его спецификация (3) ¾ однозначна. Если истинно правило FB1, то истинна следующая формула:

R(x, y) Þ LS(A(x: y))

Для условного оператора if ( C) A(x: y) else B(x: y) определим правила:

Правило FC1. R(x, y) & C ├ LS(A(x: y))

Правило FC2. R(x, y) & ØC ├ LS(B(x: y))

Лемма 9. Если истинны правила FC1 и FC2, то истинна следующая формула:

R(x, y) Þ LS(if ( C) A(x: y) else B(x: y))

Допустим A(x: z) ¾ нерекурсивный вызов предиката со спецификацией:

{P(x)} A(x: z) {Q(x, z)} (11)

Для оператора суперпозиции A(x: z); B(x, z: y) определим специализацию правил FS1 и FS2:

Правило FS5. R(x, y) ├ P(x)

Правило FS6. R(x, y) & Q(x, z) ├ LS(B(x, z: y))

Лемма 27. Допустим, нерекурсивный вызов предиката A(x: z) является корректным относительно спецификации (11). Если правила FS5 и FS6 истинны, то истинна следующая формула:

R(x, y) Þ LS(A(x: z); B(x, z: y))

Допустим, рекурсивное кольцо состоит из единственного определения предиката:

A(t, x: y) º P(t, x) { K(t, x: y) } Q(t, x, y) (5.20)

Формула корректности определения (5.20) для серии F принимает вид:

V(t) º P(t, x) & Q(t, x, y) Þ LS(K(t, x: y)) (2)

Правила корректности FR для (5.20) принимает вид:

Правило FR1. Induct(t) & P(t, x) & Q(t, x, y)├ LS(K(t, x: y)).

Лемма 14. Допустим, спецификация (предусловие P(t, x) и постусловие Q(t, x, y)) является реализуемой, а оператор K(t, x: y) ¾ однозначный. Если правило FR1 истинно, то определение (5.20) является корректным.

Пусть имеется рекурсивный вызов предиката A(u, x1: y1) в составе оператора K(t, x: y) в определении (5.20) предиката A. Для рекурсивного вызова A(u, x1: y1) определим правило:

Правило FB3. R(u, t, x1, y1) ├ Less(u, t) & P(u, x1) & Q(u, x1, y1)

Здесь предикат Less(u, t) обозначает отношение u ⊏ t или m(u) < m(t), находящееся в составе предиката Induct(t).

Лемма 17. Если истинно правило FB3, то истинна следующая формула:

Induct(t) & R(u, t, x1, y1) Þ LS(A(u, x1: y1))

Приложение 2

static const uint32_t small_limit = 17;

static const uint32_t small_sqrts[small_limit] =

// 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16

{0, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4};

#define sqrtBit(k) \

t = s + (1UL << (k - 1)); t <<= k + 1; if (_n >= t) {_n -= t; s |= 1UL << k;}

uint32_t os::isqrt(uint32_t _n) {

if (_n < small_limit)

return small_sqrts[_n];

uint32_t s = 0UL;

if (_n >= 1UL<<30) {

_n -= 1UL<<30;

s = 1UL<<15;

}

uint32_t t;

sqrtBit(14);

sqrtBit(13);

sqrtBit(12);

sqrtBit(11);

sqrtBit(10);

sqrtBit(9);

sqrtBit(8);

sqrtBit(7);

sqrtBit(6);

sqrtBit(5);

sqrtBit(4);

sqrtBit(3);

sqrtBit(2);

sqrtBit(1);

if (_n > s<<1)

s |= 1UL;

return s;

}

Приложение 3

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