В.Ш. Кауфман - Языки программирования - концепции и принципы (1990) (1160787), страница 56
Текст из файла (страница 56)
в программах. Среди них особое место принадлежит классу методов, в основе
которых лежит концепция математического доказательства правильности
программы (или короче, доказательного программирования).
Конечно, такая концепция должна подразумевать представление как самой
программы, так и требований к ней определенными математическими объектами.
Другими словами, в каждом методе доказательного программирования строится
некоторая математическая модель программы и внешнего мира (программной
среды), в котором выразимо понятие правильности программ.
Ясно, что доказательное программирование в принципе не в состоянии
полностью избавить от содержательных ошибок в програаме уже хотя бы потому,
что указанные математические модели (в том числн математическая модель
ошибки) - лишь приближение к реальному внешнему миру программы.
Вместе с тем доказательное программирование в целом получило столь
серьезное развитие, что некоторые специалисты даже склонны считать владение
им обязательным атрибутом квалифицированного программиста. Если оно и не
избавляет от ошибок, то по крайней мере может способствовать весьма
тщательному, хорошо структурированному проектированию и анализу программы.
Поскольку при этом ведется работа с точными математическими объектами,
существенная часть ее может быть автоматизирована.
В задачу книги не входит подробное изложение методов доказательного
программирования. Нет нужды конкурировать с прекрасным учебником такого
признанного мастера, как Дэвид Грис [23]. Нас интересуют прежде всего
свойства ЯП, полезные для доказательного программирования. Рассмотрим эти
свойства на примере двух методов, первый из которых (метод Бэкуса) до сих
пор не был освещен в отечественной литературе, а второй (метод Хоара)
считается классическим для этой области.
15.2. Доказательное программирование методом Бэкуса
Математическая модель программы в модели Б построена - программа
представлена функциональным выражением (формулой). Остается построить модель
внешнего мира. Он представлен алгеброй программ. С точки зрения
доказательного программирования самое важное, что можно делать с программой
в этом мире - ее можно преобразовывать по законам этой алгебры.
15.2.1. Алгебра программ в модели Б
Наша ближайшая цель - показать, как простота (скорее регулярность,
свобода от контекста) функциональных форм способствует построению системы
регулярных преобразований, сохраняющих смысл программы (построению алгебры
программ). В этой алгебре носитель (область значений переменных) - это класс
функций в модели Б, а операции - формы в модели Б. Например,
(f * g) * h
- это выражение (формула) в алгебре программ. Результат "вычисления" этого
выражения различен в зависимости от значений переменных f,g,h - при
конкретной интерпретации переменных это вполне определенная функция.
Например, при интерпретации
(f -> id,g ->
id,h -> id)
получаем
(f * g) * h = id .
В этой алгебре с программами-выражениями можно обращаться аналогично
тому, как в школьной алгебре обращаются с формулами, уравнениями,
неравенствами. Применять это умение можно для упрощения программ и
доказательства их эквивалентности (а значит и корректности, если
правильность эквивалентной программы установлена или считается очевидной).
Основой для преобразований служит серия законов. Некоторые из них мы
перечислим. Например:
(f,g) * h = ((f * h),(g * h)) .
К этим законам можно относиться либо как к аксиомам, либо как к
теоремам (например, когда рассматривается конкретная реализация форм,
например, в модели МТ). Будем относиться к перечисленным ниже законам как к
аксиомам. Лишь для одного из них в качестве примера приведем доказательство
его справедливости.
15.1.2. Законы алгебры программ
1. (f1, ... ,fn) * g = (f1 * g, ... ,fn * g)
2. A f * (g1, ... ,gn) = (f * g1, ... ,f * gn)
Здесь "А" обозначает общую аппликацию.
3. /f * (g1, ... ,gn) = f * (g1,/f * (g2, ... ,gn))
для n >= 2
/f * <g> = g
4. (f1 * 1, ... ,fn * n) * (g1, ... ,gn) =
(f1 * g1, ... ,fn * gn)
5. appendl * (f * g, Af * h) = Af * appendl (g,n)
6. pair & not * null * 1 ->->
appendl * ((1 * 1,2), distr * ( t1 * 1,2)) = distr .
7. A(f * g) = Af * Ag
Теорема. pair & not * null * 1 ->->
appendl * (( 1 * 1,2), distr * (t1 * 1,2)) = distr .
Другими словами, равенство, которое написано справа от знака "->->",
выполнено для класса объектов, удовлетворяющих условию, выписанному слева от
"->->" (т.е. для пар с непустой первой компонентой).
Доказательство. Идея : слева и справа от знака равенства получается тот
же результат для любого объекта из выделяемого условием класса.
Случай 1. x - атом или <?> .
distr : (x,y) = <?>. (см. опр distr)
t1 * 1 : (x,y) = <?>. (опр t1).
И так как все функции сохраняют <?>, получаем утверждение теоремы.
Случай 2. х = <x1, ... ,xn> (т.е. x - кортеж). Тогда
appendl * ((1 * 1,2),distr * (t1 * 1,2)) : <x,y> =
= appendl:<<1:x,y>, distr:<t1:x,y>> =
Если t1:x = <> [<> обозначает "пусто"], то
= appendl:<<x1,y>,<>> = <<x1,y>> = distr:<x,y> .
Если t1:x /= <>, то
= appendl:<<x1,y>,<<x2,y>, ... ,<xn,y>>> =
= distr:<x,y>.
Что и требовалось доказать.
15.2.2. Эквивалентность двух программ перемножения матриц
Наша ближайшая цель - продемонстрировать применение алгебры программ
для доказательства эквивалентности двух нетривиальных программ. Одна из них
- программа ММ из п.14.2.10, при создании которой мы совершенно игнорировали
проблему эффективности (в частности, расхода памяти исполнителя). Вторая -
программа MMR, которую мы создадим для решения той же задачи (перемножения
матриц), но позаботимся теперь о рациональном использовании памяти
исполнителя. Естественно, MMR получится более запутанной. Уверенность в ее
правильности (корректности) будет, конечно, более высокой, если удастся
доказать ее эквивалентность ММ, при создании которой именно правильность
(концептуальная ясность) и была основной целью.
Естественно считать ММ точной формальной спецификацией задачи
перемножения матриц (т.е. определением функции "перемножение матриц"). Тогда
доказательство эквивалентности некоторой программы, предназначенной для
решения той же задачи, программе ММ становится доказательством корректности
такой программы по отношению к спецификации (доказательством того, что эта
программа решает именно поставленную задачу, а не какую-нибудь другую).
Доказательство корректности программ по отношению к их (формальной)
спецификации часто называют верификацией программ. Таким образом, мы
продемонстрируем, в частности, применение алгебры программ для их
верификации.
Замечание. Применяемый нами метод верификации принадлежит Бэкусу и не
является общепринятым. Чаще, говоря о верификации, имеют в виду
спецификации, написанные на логическом языке, а не на функциональном. Мы
поговорим и о таких спецификациях, когда займемся так называемой дедуктивной
семантикой программ. Заметим, что все последнее время мы занимались по сути
денотационной семантикой - ведь программа в модели Б явно представляет свой
денотат (реализуемую функцию) в виде комбинации функций.
Экономная программа R перемножения матриц.
Напомним строение программы ММ:
DEF MM :: AA IP * A distl * distr * (1,trans * 2) .
Замечание. Всюду ниже для уменьшения числа скобок будем считать, что
операции "А" и "/" имеют высший приоритет по сравнению с "*" и ",". При
реализации в модели МТ этого легко добиться, поместив определения первых
операций НИЖЕ в поле определений (почему ?).
Рассмотрим программу ММ' такую, что
DEF MM' :: AA IP * A distl * distr .
Она "заканчивает" работу ММ, начиная уже с пары матриц с
транспонированной второй компонентой. Будем оптимизировать именно ММ', так
как в ней находится источник неэффективности, с которым мы намерены
бороться. Дело в том, что функция AA IP применима только к матрице пар,
которая требует памяти объемом mb + ka, где a и b - объем соответственно
первой и второй матриц, k - число столбцов второй матрицы, m - число строк
первой. Хотелось бы расходовать память экономнее.
Постараемся определить другую программу (назовем ее R) так, чтобы она
реализовала ту же функцию, что и ММ', но экономнее расходовала память.
Основная идея состоит в том, чтобы перемножение матриц представить как
последовательное перемножение очередной строки первой матрицы на вторую
матрицу. Тогда можно перемножать последующие строки НА МЕСТЕ, освободившемся
после завершения перемножения предыдущих строк, так что потребуется лишь
объем памяти, сравнимый с размером перемножаемых матриц.
Определим вначале программу mM, выполняющую перемножение первой строки
первой матрицы на вторую матрицу:
DEF mM :: A IP * distl * (1 * 1,2) .
Действительно, программа mM сначала "расписывает" строки второй матрицы
первой строкой первой матрицы (функция distl), а затем скалярно перемножает
получившиеся пары строк, что и требовалось.
Теперь определим программу R:
DEF R :: null * 1 --> const(<>);
appendl * (mM, MM' * (t1 * 1,2)) .
Таким образом, если первая матрица не пустая, то результат функции R
получается соединением в один объект (с помощью appendl) результата функции
mM (она перемножает первую строку первой матрицы на вторую матрицу) и
результата функции ММ', которая "хвост" первой матрицы перемножает на вторую
матрицу.
Заметим, что если удастся доказать эквивалентность ММ' и R, то ММ'
можно заменить на R и в определении самой R. Так что определение R через ММ'
можно считать техническим приемом, облегчающим доказательство (не придется
заниматься рекурсией). Перепишем определение R без ММ':
DEF R :: null * 1 --> const (<>);
appendl * (mM, R * (t1 * 1, 2)) .
Независимо от того, удастся ли доказать эквивалентность R и MM', ясно,
что в новом определении R отсутствует двойная общая аппликация и, если
вычислять R разумно (как подсказывает внешняя конструкция, т.е. сначала
вычислить левый ее операнд, а затем правый), то последовательные строки
матрицы-результата можно вычислять на одном и том же рабочем пространстве.
Этого нам и хотелось!
Итак, сосредоточившись на сути задачи, мы выписали ее спецификацию-
функцию, т.е. программу ММ', а концентрируясь на экономии памяти, получили
оптимизированный вариант программы, т.е. R. Займемся верификацией программы
R.
Верификация программы R. Покажем, что
R = MM'
для всех аргументов, которые нас интересуют, т.е. для всех пар. Есть
различныые способы такого доказательства. "Изюминка" модели Бэкуса состоит
в том, что для доказательства свойств программ и, в частности, их
верификации, можно пользоваться общими алгебраическими законами
(соотношениями), справедливыми в этой модели, причем для установления и
применения этих законов не нужно вводить никакого нового аппарата - все, что
нужно, уже определено в модели Б.
Докажем, что верна следующая теорема.
Теорема. pair ->-> MM' = R .
Доказательство.
Случай 1: pair & null * 1 ->-> MM' = R .
pair & (null * 1) ->-> R = const(<>) . [По определению R]
pair & (null * 1) ->-> MM' = const(<>) .
[Так как distr:<<>,X> = <> по определению distr и A f:<> = <> по
определению А]
Следовательно, ММ' = R.
Случай 2. (основной).
pair & (not * null * 1) ->-> MM' = R .
Ясно, что в этом случае R = R'', где
DEF R'' :: appendl * (mM, MM' * (t1 * 1,2)) [по определению формы
"условие"]. Расписывая mM, получаем формулу для R''
R'' = appendl * (A IP * distl * (1 * 1,2),
---- f ----- -- g --
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
