John Harrison - Введение в функциональное программирование (1108517), страница 21
Текст из файла (страница 21)
В тоже время, оба эти предположения могут оказаться неверными в некоторыхслучаях.• Верификация программы опирается на её математическую спецификацию.Возможна ситуация, когда спецификация не соответствует в точности темтребованиям, которые в действительности предъявляются к программе.На самом деле, зачастую оказывается особенно трудно сформулироватьматематически корректную версию неформальных требований. Имеетсядостаточное количество свидетельств того, что существенные проблемыкомпьютерных систем вызваны не ошибками в их реализации, а невернымпониманием ожиданий пользователей. Попытка формализации требованийчасто бывает полезной сама по себе.Сложившаяся ситуация может быть представлена диаграммой:2Например, Литлвуд доказал в 1914 г., что выражениеπ(n) − li(n), где π(n) обозначеноRnколичество простых чисел, не превышающих n, а li(n) = 0 du/ln(u), меняет свой знак бесконечноеколичество раз.
Его результат оказался крайней неожиданностью, поскольку в ходе вычисленияэтого выражения вплоть до n = 1010 не было обнаружено ни одной смены его знака.82Глава 7. Доказательство7.1. Функциональныекорректности программпрограммы как математические объектыТребования к системе6Математическая спецификация требований6Математическая модель системы6Реализация системыМы пытаемся установить связь между верхним и нижним элементами диаграммы,т.
е. между требованиями к системе и её реализацией. Чтобы добиться этойцели, нам придётся формализовать и то, и другое. Лишь одна связь надиаграмме, между математическими моделями, обладает математической жеточностью, прочие связи остаются неформальными. Всё, что мы можем сделать,это постараться сохранять максимальную простоту и прозрачность правил переходаот неформальных требований (моделей) к формальным и обратно, используяпрагматичную модель системы и высокоуровневую достаточно читабельнуюматематическую спецификацию.Однако, несмотря на эти ограничения, верификация обладает существеннымидостоинствами. В отличие от тестирования, она устанавливает корректность раз инавсегда, причём, возможно, для целого класса программ одновременно (к примеру,различающихся некоторыми параметрами). Более того, аналитический характерпроцесса верификации может привести (даже в случае неудачи) к более глубокомупониманию не только программы, но и задачи в целом.7.1Функциональныепрограммыматематические объектыкакВо введении было отмечено, что (чистые) функциональные программы напрямуюсоответствуют математическому понятию функции.
Из этого факта зачастуюделается вывод, что функциональные программы легче поддаются формальномудоказательству корректности, чем императивные. Если даже это и справедливо(с чем многие не согласятся), не следует забывать, что разрыв между математическойабстракцией и выполнением программы аппаратным обеспечением в случаефункционального подхода гораздо больше, чем для типичных императивных языков.В частности, может оказаться, что в глубинах реализации скрываются неприемлемыетребования к объёму доступной памяти. Таким образом лёгкость доказательстваможет достигаться исключением из рассмотрения существенно важных аспектов.Мы не будем обсуждать этот вопрос в данной работе, а сосредоточимся надемонстрации того, что рассуждения о простых функциональных программахзачастую оказываются тривиальными.В предыдущем разделе был приведён пример, который демонстрирует неточностьнаивного отождествления функциональных пространств ML с математическими.Однако, если мы не будем углубляться в подробности теории рекурсивных типови не рассматриваем пространство произвольных функций, а ограничимся лишь837.2.
Вычисление степениГлава 7. Доказательство корректности программнекоторыми из них, то в этом случае возможно обращаться с понятиями языка ML,как с математическими. 3Сопоставим функциональным программам математические функции. Располагаяуравнениями (обычно рекурсивными), которые определяют функции на языке ML,мы хотим интерпретировать их как аксиоматику соответствующих математическихобъектов.
Например, из определения функции факториала#let rec fact = fun 0 -> 1| n -> n * fact(n - 1);;следует, что fact(0) = 1 и что для произвольных n 6= 0 мы имеем fact(n) = n ∗ fact(n −1). Эти утверждения верны, но в дополнение к ним мы должны проявить особоевнимание к проблеме завершимости. Для отрицательных значений n программазацикливается, поэтому второе равенство можно полагать истинным лишь в томсмысле, что обе его части будут неопределёнными.
Анализ всюду определённыхфункций менее трудоёмок; в противном случае требуется отдельное доказательствозавершимости вычислений. В примерах, которые приводятся ниже, это делаетсяпараллельно с доказательством корректности, т. е. для каждого аргумента мыдолжны показать, что вычисления завершаются, причём результат удовлетворяетспецификации.В общем случае процесс доказательства может потребовать применения самыхразличных математических приёмов. Однако, очень часто свойства функций(включая завершимость), определённых рекурсивно, можно доказать по индукциив силу двойственности этих двух понятий. Более того, различные формы индукции(арифметическая, структурная, трансфинитная) обычно прямо соответствуют видамрекурсии, применённой в определении.
Ниже будут изложены примеры, поясняющиеэто утверждение.7.2Вычисление степениНапомним нашу простую реализацию вычисления степени:#let rec exp x n =if n = 0 then 1else x * exp x (n - 1);;Докажем, что exp обладает следующим свойством:Теорема 7.1 Для любого n ≥ 0 и произвольного x функция exp x n определена ипринимает значение xn .Доказательство: Функция exp была определена при помощи примитивнойпошаговой рекурсии. Как следствие, для доказательства уместно будетвоспользоваться пошаговой индукцией. Покажем, что наше утверждениесправедливо для n = 0, а затем, предположив его справедливость дляпроизвольных n ≥ 0, докажем его также и для n + 1.3Будем игнорировать возможность арифметического переполнения. CAML поддерживаетарифметику произвольной разрядности ценой, в общем случае, неограниченного расхода памяти.84Глава 7.
Доказательство корректности программ7.3. Вычисление НОД1. При n = 0 наша реализация даёт exp x n = 1. По определению, дляпроизвольного целого x имеем x0 = 1, таким образом базис индукциивыполняется. Заметим, что мы неявно предполагаем справедливость 00 =1 — хороший пример того, как тщательно нужно составлять спецификации,разрешая неоднозначности (каково значение xn в общем случае?), при этомучитывая, что некоторые люди могут быть немало удивлены нашимвыбором.2.
Предположим, что при n ≥ 0 мы имеем exp x n = xn . Из n ≥ 0 следует,что n + 1 6= 0 и, по определению, exp x (n + 1) = x ∗ exp x ((n + 1) − 1). Отсюдаexp x (n + 1) ====x ∗ exp x ((n + 1) − 1)x ∗ exp x nx ∗ xnxn+17.3Вычисление НОДРассмотримнашуреализациювычисленияделителя gcd(m, n) двух натуральных чисел m и n:наибольшегообщего#let rec gcd x y =if y = 0 then x else gcd y (x mod y);;Будем утверждать, что в действительности эта функция применима к любым целымчислам, а не только положительным. Однако, в этом случае нам понадобитсярасширенное определение понятия НОД.
Определим отношение ‘u|v’, либо ‘uявляется делителем v’, в которое входят всевозможные пары целых чисел u и v,для которых ‘v кратно u’, т. е. найдётся такое целое число d, что v = du. Например,0|0, 1|11, −2|4, но 0 6 |1, 3 6 |5. Будем говорить, что d является наибольшим общимделителем x и y, если:• d|x и d|y• Для любых других целых d0 , если d0 |x и d0 |y, то d0 |d.Отметим, что мы используем в определении d0 |d, а не d0 ≤ d. Тем самым понятие«наибольший» делитель лишается смысла, но именно так вводится его определениев алгебре.
Также заметим, что любая пара чисел (за исключением 0 и 0) имеет дванаибольших делителя, поскольку из определения следует, что если число d являетсяНОД x и y, то это же справедливо и для −d.С учётом сказанного выше, наша спецификация примет такой вид: дляпроизвольных целых чисел x и y, d = gcd x y является наибольшим общимделителем x и y. На её примере можно ещё раз убедиться, что разработкаспецификации даже такой простой функции зачастую оказывается сложнее,857.3. Вычисление НОДГлава 7. Доказательство корректности программчем ожидалось. Кроме того, данная спецификация типична ещё и в том, чтоне определяет однозначно результат вычислений, а лишь задаёт определённыеограничения.
Если мы определим функцию ngcd как#let rec ngcd x y = -(gcd x y);;то она будет точно так же удовлетворять спецификации, как и gcd. Безусловно, мыможем при необходимости сделать спецификацию более строгой. Например, еслимы ограничимся положительными значениями x и y, функция будет в полной мересоответствовать понятию наибольшего общего делителя.Функция gcd не определяется исключительно посредством примитивнойрекурсии. На шаге алгоритма Евклида gcd x y выражается через gcd y (xmod y). Соответственно, вместо пошаговой индукции будет уместно применитьтрансфинитную.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
