Э. Дейкстра Дисциплина программирования. Предисловие редактора перевода
 Скачать 1.14 Mb.
|
|
22 Э. Дейкстра. ”Дисциплина программирования” это однооператорпый язык, в котором можно описать только одну конструкцию, причем единствен- ное, что способна сделать для нас данная конструкция, это "оставить вce, как есть" (или "ничего не делать", но такое негативное употребление языка представляет опасность, см. следующий абзац). Другой простой преобразователь предикатов приводит к постоянномy слабейшему предусловию, которое вовсе не зависит от постусловия R. Мы имеем два предиката-константы, T и F . Конструк- ция S, для которой wp(S, R) = T при всех R, не может существовать, потому что она нарушила бы закон исключенного чуда. Однако конструкция S, для которой wp(S, R) = F при всех R, облада- ет преобразователем предикатов, удовлетворяющим всем необходимым свойствам. Этому оператору мы тоже присвоим имя, назовем его "отказать". Итак, семантика оператора "отказать" задается следующим образом: wp(отказать, R) = F для любого постусловия R Этот оператор не может даже "ничего не делать" в смысле "оставить все, как есть"; он вообще ни на что не способен. Если мы полагаем R = T , т. е. не накладываем на конечное состояние никаких дополнительных требований, кроме самого факта его существования, даже тогда не найдется соответ- ствующего начального состояния. Если запустить конструкцию по имени "отказать", она не сможет достичь конечного состояния: сама попытка ее запуска является гарантией неудачи. (Нас не должно занимать теперь (а также и впоследствии) то, что позднее мы введем структуру операторов, в которой содержатся как частные случаи семантические эквиваленты для "пропустить" и "отказать".) Теперь мы располагаем неким (все еще весьма зачаточным) двухоператорным языком програм- мирования, в котором можем описать две конструкции; одна из них ничего не делает, а вторая всегда терпит неудачу. Со времени опубликования знаменитого "Собщения об алгоритмическом языке АЛ- ГОЛ 60" в 1960 г. никакой уважающий себя ученый, занимающийся программированием, не позво- лит себе обойтись на этом этапе без формального определения синтаксиса столь далеко продвинутого языка программирования в системе обозначений, называемой "НФБ" (сокращение от "Нормальная форма Бэкуса"), а именно: оператор ::= пропустить|отказать (Читается так: "Элемент синтаксической категории, именуемой "оператор" (именно это обозначают забавные скобки "<" и ">"), определяется как (это обозначает знак "::=") "пропустить" или (это обо- значает вертикальная черта " |") "отказать". Колоссально! Но не беспокойтесь; более впечатляющие применения НФБ в качестве способа записи последуют в надлежащее время.) Один класс безусловно более интересных преобразователей предикатов основывается на подста- новке, т. е. на замене всех вхождений некоей переменной в формальном выражении для постусловия R на (одно и то же) "что-нибудь другое". Если в предикате R все вхождения переменной x заменяются некоторым выражением (E), то мы обозначаем результат этого преобразования через R E→X . Теперь мы можем рассмотреть для заданных x и E такую конструкцию, чтобы для любых постусловий R получалось wp(S, R) = R E→X ; здесь x — "координатная переменная" нашего пространства состояний, а E — выражение соответствующего типа. Замечание. Такое преобразование путем подстановки удовлетворяет свойствам 1–4 из предыду- щей главы. Мы не станем пытаться демонстрировать это и предоставим самому читателю решать в зависимости от своего вкуса, будет ли он относиться к этому как к тривиальному или же как к глубокому математическому результату. (Конец замечания.) Таким способом вводится целый класс преобразователей предикатов, целый класс конструкций. Они обозначаются оператором, который называется "оператор присваивания"; такой оператор дол- жен определять три вещи: 1) наименование переменной, подлежащей замене; 2) тот факт, что правило, соответствующее преобразованию предикатов, есть подстановка; 3) выражение, которым должно заменяться всякое вхождение этой переменной в постусловии. Если переменная x должна быть заменена выражением (E) то обычная запись такого оператора выглядит следующим образом: x := E (где так называемый знак присваивания ":=" следует читать как "становится"). Сказанное можно суммировать, определив wp("x := E", R) = R E→X Для любого постусловия R При желании это можно рассматривать как семантическое определение оператора присваивания для любой координатной переменной x и любого выражения E соответствующего типа. Наслаждаясь, Э. Дейкстра. ”Дисциплина программирования” 23 по нашему обыкновению, употреблением НФБ, мы можем расширить наш формальный синтаксис, чтобы он читался так: оператор ::= пропустить|отказать| оператор присваивания оператор присваивания ::= переменная := выражение причем последнюю строчку следует читать так: "Элемент синтаксической категории, именуемой "оператор присваивания", определяется как элемент синтаксической категории, именуемой "пере- менная", за которым следуют сначала знак присваивания ":=", а затем элемент синтаксической кате- гории, именуемой "выражение". Перед тем как продолжить рассуждение, представляется разумным убедиться в том, что этим формальным описанием оператора присваивания в самом деле охваты- вается наше интуитивное понимание оператора присваивания — если оно у нас есть! Рассмотрим пространство состояний с двумя целыми координатными переменными "a" и "b". Тогда wp("a := 7", a = 7) = {7 = 7} и, поскольку логическое выражение в правой части является истиной для всех значений a и b, т. е. для всех точек пространства состояний, мы можем упрощенно записать это так: wp("a := 7", a = 7) = T Иначе говоря, всякое начальное состояние гарантирует, что присваивание "a := 7" обеспечит истин- ность "a = 7". Аналогично wp("a := 7", a = 6) = {7 = 6} и, поскольку это логическое выражение является ложью для всех значений a и b, мы получаем wp("a := 7", a = 6) = F Это означает, что не существует никакого начального состояния, для которого мы могли бы гарантировать, что присваивание "a := 7" обеспечит истинность "a = 6". (Это находится в сооветствии с нашим предыдущим результатом, что все начальные состояния обеспечат конечную истинность "a = 7", а следовательно, конечную ложность "a = 7".) Далее, wp("a := 7", b = b0) = {b = b0} т. е. если мы хотим гарантировать, что после присваивания "a := 7" переменная b имеет некоторое значение b0, то нужно, чтобы b имела это значение еще в начальном состоянии. Другими словами, все переменные, за исключением "a", не изменяются, они сохраняют те значения, которые имели раньше; присваиванне "a := 7" перемещает в пространстве состояний точку, соответствующую теку- щему состоянию системы, параллельно оси a так, что обеспечивается конечное выполнение равенства "a = 7". Вместо того чтобы брать в качестве выражения E константу, мы могли бы взять какую-то функ- цию от начального состояния. Это иллюстрируется следующими примерами: wp("a := 2 ∗ b + 1", a = 13) = {2 ∗ b + 1 = 13} = {b = 6} wp("a := a + 1", a > 10) = {a + 1 > 10} = {a > 9} wp("a := a − b", a > b) = {a − b > b} = {a > 2 ∗ b} Возникает небольшое осложнение, если мы разрешаем выражению E быть частично определен- ной функцией начачального состояния, т. е. такой функцией, попытка вычисления которой для начального состояния, не входящего в область определения, не приведет к правильно завершаемой работе. Если мы хотим предусмотреть и эту ситуацию, то нам нужно уточнить наше определение семантики оператора присваиваивания и записать wp("x := E", R) = {D(E) cand R E→X } Здесь предикат D(E) означает "в области определения E"; логическое выражение "B1 cand B2" (так называемая "условная конъюнкция") имеет то же значение, что и "B1 and B2", если оба операнда определены, но помимо этого по определению оно имеет значение "ложь", если B1 является "ложью"; последнее справедливо вне зависимости от того, определен ли операнд B2. Обычно условие D(E) не 24 Э. Дейкстра. ”Дисциплина программирования” подчеркивается явно либо потому, что оно=T , либо потому, что мы исходим из предположения, что оператор присваивания никогда не будет запущен в начальных состояниях, не принадлежащих области определения выражения E. Естественным обобщением оператора присваивания является излюбленное некоторыми програм- мистами так называемое "одновременное присваивание". В этом случае возможна одновременная замена для нескольких различныхпеременных. Оператор одновременного присваивания обозначает- ся списком различных переменных), подлежащих замене (эти переменные разделяются запятыми), слева от знака присваивания и столь же протяженным списком выражений (также разделяемых запятыми) справа от знака присваивания. Итак, разрешается писать x1, x2 := E1, E2 x1, x2, x3 := E1, E2, E3 Заметим, что i-я переменная из списка левой части должна быть заменена на i-e выражение из списка правой части, так что, например, при заданных x1, x2, E1 и E2 оператор x1, x2 := E1, E2 семантически эквивалентен оператору x2, x1 := E2, E1 Одновременное присваивание позволяет нам предписать, чтобы две переменные x и y обменялись своими значениями с помощью оператора x, y := y, x В иной записи эта операция выглядела бы более громоздкой. Легкость реализации одновременного присваивания и возможность с его помощью избегать некоторой избыточности записи являются при- чинами популярности таких операторов. Заметим, что если списки становятся слишком длинными, то получаемая программа становится весьма неудобочитаемой. Истинный любитель НФБ расширит свой синтаксис, обеспечив две различные формы для опера- тора присваивания, следующим образом: оператор присваивания ::= переменная := выражение | переменная , оператор присваивания , выражение Это так называемое "рекурсивное определение", поскольку одна из альтернативных форм для син- таксической единицы, именуемой "оператор присваивания" (а именно вторая форма), содержит в качестве одного из своих компонентов снова эту же синтаксическую единицу, именуемую "оператор присваивания", т. е. ту самую синтаксическую единицу, которую мы определяем! На первый взгляд такое циклическое определение выглядит ужасающе, но после более внимательного изучения мы можем убедиться в том, что, по крайней мере с синтаксической точки зрения, в этом нет ничего неправильного. Например, поскольку, согласно первой альтернативе, x2 := E1 является примером оператора присваивания, то формула x1, x2 := E1, E2 допускает разбор вида x1, оператор присваивания , E2 а следовательно, согласно второй альтернативе, также является оператором присваивания. Однако с семантической точки зрения это отвратительно, потому что получается, что E2 ассоциируется с x1 вместо того, чтобы ассоциироваться с x2. В сравнении с двухоператорным языком, содержащим только "пропустить" и "отказать", наш язык с оператором присваивания выглядит значительно более богатым: уже нет какой бы то ни было верхней границы для числа различных примеров синтаксической единицы "оператор присва- ивания". Но он все же явно недостаточен для наших целей; нам нужна возможность строить более Э. Дейкстра. ”Дисциплина программирования” 25 изощренные программы, более сложные конструкции. Для построения потенциально сложных кон- струкций мы пользуемся схемой, которую можно рекурсивно описать так: конструкция ::= простая конструкция | правильная композиция записей вида: конструкция Для того чтобы эта схема могла принести хоть какую-нибудь пользу, необходимо выполнение двух условий: в нашем распоряжении должны иметься "простые конструкции", чтобы было с чего начать, и, кроме того, мы должны знать, как строить "правильные композиции". Введенные раньше операторы можно взять в качестве простых конструкций; оставшаяся часть этой главы посвящена именно процессу правильной композиции некоей новой конструкции из заданных конструкций. Новая конструкция в свою очередь может выступать в роли части еще более сложного составного объекта. После того, как объект был образован композицией частей, мы можем рассматривать его двумя способами. Во-первых, мы можем считать его "нераздельным целым", воспринимая его свойства в большей или меньшей степени как магические (или принимая их на веру или как постулаты). При таком подходе существенны только свойства конструкции; не имеет никакoro значения, каким об- разом она образована из своих частей. С такой точки зрения любые две конструкции, обладающие одинаковыми свойствами, эквивалентны. Или же мы рассматриваем конструкцию как "составной объект", образованный так, что мы можем понять, почему она обладает объявленными свойствами. При этом мы воспринимаем части как "малые" нераздельные целые, для которых принимаются в расчет только их общие свойства. Второй подход вносит ясность в то, что мы понимаем под "компо- зицией". Композиция должна определять, как свойства целого следуют из свойств частей. После этих общих замечаний вернемся к нашим конкретным конструкциям, свойства которых, как мы считаем, выражаются их преобразователями предикатов. Точнее говоря, если заданы две конструкции S1 и S2, чьи преобразователи предикатов известны, можем ли мы представить себе правило вывода нового преобразователя предикатов из двух заданных? Если да, то мы можем считать результирующий преобразователь предикатов описанием свойств составного объекта, построенного специальным образом из частей S1 и S2. Одним из простейших способов получения новой функции из двух заданных является так на- зываемая "функциональная композиция", т. е. предоставление значения одной функции в качестве аргумента для другой. Составной объект, соответствующий такому преобразователю предикатов, принято обозначать через "S1; S2", и мы определяем wp("S1; S2", R) = wp(S1, wp(S2, R)) что при желании можно рассматривать как семантическое определение точки с запятой. Замечанue. Из того факта, что преобразователи предикатов для S1 и S2 обладают свойствами 1–4 из предыдущей главы, можно заключить, что и определенный выше преобразователь предикатов для "S1; S2" также обладает этими четырьмя свойствами. Например, поскольку для S1 и S2 справедлив закон исключенного чуда: wp(S1, F ) = F и wp(S2, F ) = F мы заключаем, подставляя F вместо R в верхнее определение что wp("S1; S2", F ) = wp(S1, wp(S2, F )) = wp(S1, F ) = F Читателю предоставляется в качестве упражнения проверить, что остальные три свойства тоже сохраняются. (Конец замечания.) Перед тем как продолжить наши рассуждения, убедимся в том, что этим формальным описани- ем семантики точки с запятой охватывается наше интуитивное представление о ней (если оно у нас есть!), т. е. что составная конструкция "S1; S2" может быть реализована но правилу "сначала запу- стить конструкцию S1 и пo окончании ее работы запустить S2". В самом деле, в нашем определении wp("S1; S2", R) мы представляем R-постусловие для составной конструкции — как постусловие к преобразователю предикатов для S2, и этим отражается то, что общая работа конструкции "S1; S2" может закончиться с окончанием работы S2. Соответствующее слабейшее предусловие для S2, т. е. wp(S2, R), представляется как постусловие к преобразователю предикатов для S1; тем самым мы 26 Э. Дейкстра. ”Дисциплина программирования” явно отождествляем начальное состояние для S2 с конечным состоянием для S1. Однако именно так и бывает, если работа S1 непосредственно предшествует во времени запуску S2. Чтобы удостовериться в этом, рассмотрим пример. Пусть "S1; S2" представляет собой "a := a + b; b := a ∗ b" и пусть нашим постусловием является некоторый предикат R(a, b); в таком случае wp(S2, R(a, b)) = wp("b := a ∗ b", R(a, b)) = R(a.c ∗ b) и wp("S1; S2", R(a, b)) = wp(S1, wp(S2, R(a, b))) = wp(S1, R(a, a ∗ b)) = wp("a := a + b", R(a, a ∗ b)) = R(a + b, (a + b) ∗ b) т.е мы можем гарантировать выполнение отношения R между конечными значениями a и b при условии, что первоначально то же отношение выполняется между a + b и (a + b) ∗ b соответственно. И наконец, поскольку функциональная композиция обладает свойством ассоциативности, то не имеет значения, будем ли мы разбирать "S1; S2; S3" как "[S1; S2]; S3" или же как "S1;[S2;S3]". Иначе говоря, мы имеем полное право трактовать точку с запятой как символ сочленения; поэтому не возникает никакой неопределенности, когда мы выписываем операторный список вида "S 1 ; S 2 ; S 3 ; . . . ; S n ", и мы будем без стеснения поступать так, когда для этого представятся подходящие случаи. Упражнение. Проверьте, что конструкции "x1 := E1; x2 := E2" и "x2 := E2; x1 := E1" семантически эквивалентны, если переменная x1 не встречается в выражении E2, а переменная x2 не встречается в выражении E1. На самом деле, в таком случае обе эти конструкции семантически эквивалентны одновременному присваиванию "x1, x2 := E1, E2". (Эта эквивалентность является од- ним из аргументов в пользу одновременного присваивания; ее применение позволяет нам избежать избыточности последовательной записи, болee того, при одновременном присваивании становится очевидным, что два выражения E1 и E2 могут вычисляться одновременно, и это последнее обсто- ятельство представляет интерес при некоторых методиках реализации. Помимо того, быть может, более интересная возможность, что конструкция "x1, x2 := E1, E2" не окажется семантически эк- вивалентной ни конструкции "x1 := E1; x2 := E2", ни конструкции "x2 := E2; x1 := E1".) (Конец упражнения.) До введения точки с запятой мы могли писать только однооператорные программы; с помощью точки с запятой мы обрели способность писать программы в виде сочленения из n, (n > 0) опера- торов: "S 1 ; S 2 ; S 3 ; . . . ; S n ". Если исключить промежуточную незавершенность, выполнение каждой программы всегда означает временную последовательность выполнений n операторов, сначала S 1 , потом S 2 и так далее до S n включительно. Однако из нашего примера игры на листе картона, реали- зующей алгоритм Евклида, мы знаем, что должны уметь описывать более широкий класс "правил игры": всякая игра будет состоять из последовательности перемещений, где каждое перемещение имеет вид либо "x := x − y", либо "y := y − x", но способ чередования этих перемещений во времени и даже их общее число будут изменяться от игры к игре; он зависит от начального положения фишки, он зависит от начального состояния системы. Если точка с запятой является единственным нашим средством для составления нового целого из заданных частей, то мы не в состоянии этого выразить, и поэтому нам необходимо искать нечто новое. Пока точка с запятой остается единственным имеющимся в нашем распоряжении средством со- единения, единственным обстоятельством, при котором происходит запуск одной из составляющих конструкций S i (i > 1), являются правильное завершение работы (лексикографически) предшеству- ющей конструкции. Чтобы добиться нужной нам гибкости, необходимо обеспечить возможность запуска той или иной (под) конструкции в зависимости от текущего состояния системы. Для этого мы введем — в два этапа — понятие "охраняемой команды", синтаксис которой задается следующим образом: охраняющий заголовок ::= логическое выражение → оператор охраняемая команда ::= охраняющий заголовок {; оператор } |