Студопедия

КАТЕГОРИИ:


Архитектура-(3434)Астрономия-(809)Биология-(7483)Биотехнологии-(1457)Военное дело-(14632)Высокие технологии-(1363)География-(913)Геология-(1438)Государство-(451)Демография-(1065)Дом-(47672)Журналистика и СМИ-(912)Изобретательство-(14524)Иностранные языки-(4268)Информатика-(17799)Искусство-(1338)История-(13644)Компьютеры-(11121)Косметика-(55)Кулинария-(373)Культура-(8427)Лингвистика-(374)Литература-(1642)Маркетинг-(23702)Математика-(16968)Машиностроение-(1700)Медицина-(12668)Менеджмент-(24684)Механика-(15423)Науковедение-(506)Образование-(11852)Охрана труда-(3308)Педагогика-(5571)Полиграфия-(1312)Политика-(7869)Право-(5454)Приборостроение-(1369)Программирование-(2801)Производство-(97182)Промышленность-(8706)Психология-(18388)Религия-(3217)Связь-(10668)Сельское хозяйство-(299)Социология-(6455)Спорт-(42831)Строительство-(4793)Торговля-(5050)Транспорт-(2929)Туризм-(1568)Физика-(3942)Философия-(17015)Финансы-(26596)Химия-(22929)Экология-(12095)Экономика-(9961)Электроника-(8441)Электротехника-(4623)Энергетика-(12629)Юриспруденция-(1492)Ядерная техника-(1748)

Синтез программ вычисления целочисленного квадратного корня




Целая часть квадратного корня есть функция: m = isqrt(x) = floor(), где z = floor(t) – целая часть вещественного аргумента t со спецификацией t <= z < t+1. Спецификацией для t = является формула t^2 = x. Таким образом, функция isqrt имеет спецификацию:

formula Isqrt(nat x, m) = m^2 <= x & x < (m + 1)^2;

isqrt(nat x: nat m) post Isqrt(x, m);

Синтез программы isqrt управляется обычным процессом построения программы по технологии предикатного программирования. При этом программа извлекается из доказательства формулы корректности (3), то есть формулы вида: Isqrt(x, m) Þ LS(S(x: m)) для некоторого оператора S(x: m). Кроме того, необходимо доказать тотальность спецификации, а именно – лемму:

Isqrt_total: lemma exists nat m. Isqrt(x, m).

Сначала синтезируем простейшую программу, определяющую результат m последовательным перебором, начиная с нуля. Для построения программы применяется метод обобщения исходной задачи isqrt. Рассмотрим задачу sq0, определяемую спецификацией:

formula P_sq0(nat x, k) = k^2 <= x;

sq0(nat x, k: m) pre P_sq0(x, k) post Isqrt(x, m);

Задача isqrt(x: m) сводится к sq0(x, 0: m), что определяет программу:

isqrt(nat x: nat m) { sq0(x, 0: m) } (5)

post Isqrt(x, m);

Корректность программы (5) доказывается по правилу FB1:

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

Истинность правила гарантирует истинность формулы R(z, y) Þ LS(A(z: y)) при условии, что предикат A(z: y) является корректным относительно однозначной спецификации [P(z), Q(z, y)]. Таким образом, требуется доказать лемму:

Isqrt_fb1: lemma Isqrt(x, m) Þ (6) P_sq0(x, 0) & Isqrt(x, m).

Разработчик программы должен записать эту лемму и доказать ее, а система автоматически, используя правило FB1 в качестве шаблона, должна синтезировать программу (5) по формуле (6). Следующей целью является синтез программы sq0 из доказательства формулы

P_sq0(x, k) & Isqrt(x, m) Þ LS(S1(x, k: m))

для некоторого оператора S1(x, k: m). Отметим, что предусловие P_sq0(x, k) обеспечивает истинность первого конъюнкта в Isqrt(x, m), а в случае истинности условия x < (k + 1)^2 получим решение задачи sq0: m = k. Задача sq0 делится на две: для истинного значения условия x < (k + 1)^2 и для ложного, что определяет поиск решения S1(x, k: m) в виде оператора if ( x < (k + 1)^2) m = k else B(x, k: m) для некоторого B(x, k: m). Корректность условного оператора доказывается правилом:

Правило FC. R(z, y) ├ (C Þ LS(A(z: y))) &

(ØC Þ LS(B(z: y))).

Истинность правила гарантирует истинность R(z, y) Þ LS(if ( C) A(z: y) else B(z: y)). Заметим, что ложное условие x < (k + 1)^2 эквивалентно P_sq0(x, k+1), а поскольку истинно Isqrt(x, m), то решение B(x, k: m) следует определить в виде рекурсивного вызова sq0(x, k + 1: m). Доказательство корректности рекурсивного вызова предиката реализуется правилом FB3, аналогичным FB1, с дополнительным условием: аргументы рекурсивного вызова должны быть по некоторой мере строго меньше аргументов определяемого рекурсивного предиката, где мера – натуральная функция от значений аргументов. В нашем случае мера e определяется формулой:

formula e(nat x, k: nat) = (x<(k + 1)^2)? 0: x – k^2;

Таким образом, корректность условного оператора с рекурсивным вызовом определяется леммой:

sq0_rec: lemma P_sq0(x, k) & Isqrt(x, m) Þ (x < (k + 1)^2)? m = k: e(x, k+1) < e(x, k) & P_sq0(x, k+1) & Isqrt(x, m).

По данной формуле, используя в качестве шаблонов правила FC и FB3, система должна автоматически синтезировать рекурсивную программу:

sq0(nat x, k: nat m) pre P_sq0(x, k)

{ if (x < (k + 1)^2) m = k else sq0(x, k + 1: m) }

post Isqrt(x, m);

Заметным недостатком алгоритма sq0 является вычисление квадрата в выражении (k + 1)^2. Поскольку (k + 1)^2=p =k^2 + 2* k + 1, то можно использовать значение k^2, вычисленное на предыдущем шаге, введением дополнительного параметра n = k^2. Аналогичным образом, введя параметр d = 2* k + 1, можно заменить умножение сложением. Далее, поскольку x < (k + 1)^2 эквивалентно x - k^2 < 2* k + 1, то вместо x и n можно использовать один параметр y = x - k^2. Таким образом, переходим к более общей задаче, определяемой спецификацией предиката sq1:

formula P_sq1(nat x, y, k, d) =

k^2 <= x & d = 2 * k + 1 & y = x - k^2;

sq1(nat x, y, k, d: nat m)

pre P_sq1(x, y, k, d) post Isqrt(x, m);

Результатом синтеза, проводимого по той же схеме, является программа:


isqrt(nat x: nat m) { sq1(x, x, 0, 1: m) }

post Isqrt(x, m);

sq1(nat x, y, k, d: nat m) pre P_sq1(x, y, k, d)

{ if (y < d) m = k

else sq1(x, y – d, k + 1, d + 2: m)

} post Isqrt(x, m);

Программа sq1 неэффективна: число шагов равно значению квадратного корня. Более эффективные алгоритмы имеют логарифмическую оценку. Рассмотрим алгоритм на базе двоичного представления аргумента, предполагая, что аргумент n ограничен значением 22*p для некоторого p > 0.

Представим исходную задачу спецификацией:

formula P_sqp(nat n, p) = p > 0 & n < 2^(2*p);

isqrt1(nat n, p: nat s) pre P_sqp(n, p)

post Isqrt(n, s);

Алгоритм определяет цифры результата, начиная со старшей и далее. Результат s имеет не более p двоичных цифр. Значение старшей цифры равно 0, если n < 2^(2*(p-1)) и 1 – в противном случае. Следующая цифра есть 0, если n < 2^(2*(p-2)) и 1 – в противном случае.

Допустим, для результата s найдено очередное приближение q в виде старших двоичных цифр с номерами от p до k. Тогда должно выполняться условие q^2 <= n < (q + 2^k)^2. Это определяет спецификацию обобщенной задачи:

formula P_sq2(nat n, p, k, q) =

P_sqp(n, p) & k <= p &

q^2 <= n & n < (q + 2^k)^2;

sq2(nat n, p, k, q: nat s) pre P_sq2(n, p, k, q)

post Isqrt(n, s);

Справедлива следующая лемма:

Isqrt1_fb1: lemma P_sqp(n, p) & Isqrt(n, s) Þ P_sq2(n, p, p, 0) & Isqrt(n, s)

По данной формуле, используя правило FB1 в качестве шаблона, система синтезирует:

isqrt1(nat n, p: nat s) pre P_sqp(n, p)

{ sq2(n, p, p, 0: s) } post Isqrt(n, s);

Заметим, что при k = 0 решением задачи sq2 будет s = q. Если в s цифра с номером k-1 есть 1, то следующим приближением для q будет q + 2^(k-1). Если n < (q + 2^(k-1))^2, то цифра с номером k-1 есть 0, иначе 1. Данные утверждения суммируем в виде леммы:

formula e2(k: nat) = k;sq2_rec: lemma P_sq2(n, p, k, q) & Isqrt(n, s) Þ (k = 0)? s = q: (n < (q + 2^(k-1))^2)? e2(k-1) < e2(k) & P_sq2(n, p, k-1, q)& Isqrt(n, s): e2(k-1) < e2(k) & P_sq2(n, p, k-1, q + 2^(k-1)) & Isqrt(n, s).

Разработчик должен доказать лемму, а система, используя в качестве шаблонов правила FC и FB3, должна автоматически синтезировать программу:

sq2(nat n, p, q, k: nat s) pre P_sq2(n, p, k, q)

{ if (k = 0) s = q

else if (n < (q + 2^(k-1))^2)

sq2(n, p, k - 1, q: s)

else sq2(n, p, k - 1, q + 2^(k-1): s)

} post Isqrt(n, s);

В выражении q + 2^(k-1) можно заменить “+” побитовой операцией “ or ”. Чтобы обеспечить корректность такой замены, необходимо доказать лемму:

or_eq_plus: lemma k > 0 & k < p & mod(q, 2^k) = 0 & q < 2^p Þ (q or 2^(k - 1)) = q + 2^(k - 1).

Необходимое условие mod(q, 2^k) = 0 проще обеспечить включением его в предусловие. Условие n < (q + 2^(k-1))^2 эквивалентно: n - q^2 < 2^((k-1)*2) + q * 2^k. Используя технику построения алгоритма sq1, обозначим y = n - q^2. Далее можно синтезировать программу с данными оптимизациями:

formula P_sq3(nat n, p, k, q, y) =

P_sq2(n, p, k, q) & y = n - q^2 &

mod(q, 2^k) = 0;

isqrt1(nat n, p: nat s) pre P_sqp(n, p)

{ sq3(n, p, p, 0, n: s) }

post Isqrt(n, s);

sq3(nat n, p, k, q, y: nat s)

pre P_sq3(n, p, k, q, y)

{ if (k = 0) s = q

else { nat t = 2^((k-1)*2) + q * 2^k;

if (y < t) sq3(n, p, k - 1, q, y: s)

else sq3(n, p, k - 1, q or 2^(k-1), y – t: s)

}

} post Isqrt(n, s);

Для рассматриваемой предикатной программы применяется последовательность трансформаций. На первом этапе реализуются склеивания переменных в sq3: n y; s q. На втором этапе хвостовая рекурсия заменяется циклом. На третьем этапе тело определения sq3 поставляется на место вызова в isqrt1 и реализуются упрощения. В итоге получим программу на императивном расширении языка P:

isqrt1(nat n, p: nat s) {

s = 0;

for (nat k = p; k = 0; k = k - 1) {

nat t = 2^((k-1)*2) + s * 2^k;

if (n >=t) { n = n – t; s = s or 2^(k-1); }

}

}

Далее, умножение на степень двойки заменяется операцией сдвига влево. Для конкретного p = 16 проведем развертку цикла, представив тело цикла макросом sq(k). Специализируем первый и последний шаг цикла. Получим окончательную программу:

 

isqrt1(nat n, p: nat s) {

sq(nat k) =

{ t = 2^((k-1)*2) + (s<<k);

if (n >=t) { n = n – t; s = s or (1<<(k-1)) }

};

s = 0;

if (n >= 2^((p-1)*2))

{ n = n – 2^((p-1)*2); s = 2^(p-1) };

sq(p – 1); …; sq(2);

if (n >= s * 2) s = s or 1;

}

По сравнению с программой, представленной на сайте:

http://www.finesse.demon.co.uk/steven/sqrt.html, параметр k смещен на единицу. Однако поскольку тело sq(k) подставляется открыто на место вызовов sq(p – 1), …, sq(2), то обе программы идентичны.




Поделиться с друзьями:


Дата добавления: 2015-06-27; Просмотров: 396; Нарушение авторских прав?; Мы поможем в написании вашей работы!


Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет



studopedia.su - Студопедия (2013 - 2024) год. Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав! Последнее добавление




Генерация страницы за: 0.032 сек.