Э. Дейкстра Дисциплина программирования. Предисловие редактора перевода
 Скачать 1.14 Mb.
|
|
16 Э. Дейкстра. ”Дисциплина программирования” Если система (машина, конструкция) обозначается через S, а желаемое постусловие — через R, то соответствующее слабейшее предусловие мы обозначим 1 wp(S, R) Если начальное состояние удовлетворяет wp(S, R), то конструкция обязательно обеспечит в конце концов истинность R. Поскольку wp(S, R) — это слабейшее предусловие, мы знаем также, что если начальное состояние не удовлетворяет wp(S, R), то такой гарантии дать нельзя, т. е. ход событий может привести к завершению работы в конечном состоянии, нe удовлетворяющем R, а может даже и вообще помешать достижению какого бы то ни было конечного состояния (как мы увидим далее, либо потому, что система оказывается вовлеченной в выполнение незавершимого задания, либо потому, что система попадает в тупик). Мы считаем, что нам достаточно хорошо известно, как работает конструкция S, если можем вывести для любого постусловия R соответствующее слабейшее предусловие wp(S, R), поскольку тем самым мы уловили, чт ´о эта конструкция способна сделать для нас; это называется "ее семантикой". Здесь уместны два замечания. Во-первых, множество возможных постусловий, вообще говоря, столь огромно, что эта информация в табличной форме (т. е. в виде таблицы, где каждому постусло- вию R соответствует запись, в которой содержится соответствующее предусловие wp(S, R)), оказалась бы совершенно необозримой, а следовательно, бесполезной. Поэтому определение семантики той или иной конструкции всегда дается другим способом — в виде правила, описывающего, как для любо- го заданного постусловия R можно вывести соответствующее слабейшее предусловие wp(S, R)). Для фиксированной конструкции S такое правило, которое по заданному предикату R, означающему по- стусловие, вырабатывает предикат wp(S, R), означающий соответствующее слабейшее предусловие, называется "преобразователем предикатов". Когда мы просим, чтобы нам сообщили описание семан- тики конструкции S, то в сущности речь идет о соответствующем этой конструкции преобразователе предикатов. Во-вторых,— и я чувствую искушение добавить "благодаря судьбе" — часто нас не интересует полная семантика конструкции. Это объясняется тем, что мы стремимся использовать конструк- цию S только для конкретной надобности, а точнее, для того, чтобы обеспечить истинность весьма конкретного постусловия R, ради которого производилась разработка конструкции. И даже приме- нительно к этому конкретному постусловию R нас часто не интересует точный вид wp(S, R); зачастую мы удовлетворяемся более сильным условием P , т. е. таким условием, для которого можно показать, что утверждение P ⇒ wp(S, R) для всех состояний (3) справедливо. (Предикат "P ⇒ Q" (читается "из P следует Q") ложен только в тех точках простран- ства состояний, где условие P справедливо, a Q не справедливо; во всех остальных точках он истинен. Требуя, чтобы утверждение "P ⇒ wp(S, R)" было справедливо для всех состояний, мы тем самым тре- буем, чтобы всякий раз когда P — истина, условие wp(S, R) тоже было истиной; тогда P — достаточ- ное предусловие. В теоретико-множественной терминологии это означает, что множество состояний, характеризуемое условием P , является подмножеством того множества состояний, которое характе- ризуется условием wp(S, R).) Если для заданных P , S и R отношение (3) выполняется, это часто можно доказать, не прибегая к точной формулировке,— или, если вам так больше нравится, "вычислению" или "выводу" — предиката wp(S, R). И это отрадное обстоятельство, поскольку, за исключением три- виальных случаев, следует ожидать, что явная формулировка условия wp(S, R) превысит по крайней мере резерв нашей писчей бумаги, нашего терпения или нашей (аналитической) изобретательности (или какую-то комбинацию этих резервов). Смысл wp(S, R), т. е. "слабейшего предусловия для начального состояния, при котором запуск обязательно приведет к событию правильного завершения, причем система S останется в конечном состоянии, удовлетворяющем постусловию R" позволяет нам установить, что преобразователь пре- дикатов, рассматриваемый как функция от постусловия R, обладает рядом определенных свойств. Свойство 1. Для любой конструкции S мы имеем wp(S, F ) = F (4) Предположим, что оказалось не так; при этом нашлось хоть одно состояние, удовлетворяющее условию wp(S, F ). Возьмем такое состояние в качестве начального состояния для конструкции S. Тогда, согласно нашему определению, запуск привел бы к событию правильного завершения, при- чем система осталась бы в конечном состоянии, удовлетворяющем предикату F . Но здесь возникает 1 По начальным буквам английских слов weakest рrе-condition.— Прим. перев. Э. Дейкстра. ”Дисциплина программирования” 17 противоречие, так как по определению предиката F не существует состояний, удовлетворяющих F ; тем самым доказано отношение (4). Свойство 1 известно также под названием "закон исключенного чуда". Свойство 2. Для любой конструкции S и любых постусловий Q и R, таких, что Q ⇒ R для всех состояний справедливо также отношение wp(S, Q) ⇒ wp(S, R) для всех состояний (6) В самом деле, при любом начальном состоянии, удовлетворяющем wp(S, Q), согласно определению, по окончании работы системы будет обеспечена истинность Q. С учетом отношения (5) тем самым будет обеспечена и истинность R. Следовательно, данное начальное состояние будет одновременно удовлетворять и условию wp(S, R), как записано в (6). Свойство 2 — это свойство монотонности. Свойство 3. Для любой конструкции S и для любых постусловий Q и R справедливо (wp(S, Q) and wp(S, R)) = wp(S, Q and R) (7) В любой точке пространства состояний из левой части отношения (7) логически следует его правая часть потому, что для любого начального состояния, удовлетворяющего wp(S, Q), и wp(S, R), мы знаем в совокупности, что установится конечное состояние, удовлетворяющее и Q, и R. Далее, поскольку, в силу определения, (Q and R) ⇒ Q для всех состояний свойство 2 позволяет нам заключить, что wp(S, Q and R) ⇒ wp(S, Q) для всех состояний и аналогично wp(S, Q and R) ⇒ wp(S, R) для всех состояний Однако из A ⇒ B и A ⇒ C, согласно исчислению предикатов, можно вывести, что A ⇒ (B and C). Поэтому правая часть отношения (7) логически следует из его левой части в любой точке пространства состояний. Поскольку обе части всюду следуют друг из друга, они должны быть равны, а тем самым доказано свойство 3. Свойство 4. Для любой конструкции S и любых постусловий Q и R справедливо (wp(S, Q) or wp(S, R)) ⇒ wp(S, Q or R) для всех состояний (8) Поскольку, в силу определения, Q ⇒ (Q or R) для всех состояний свойство 2 позволяет нам прийти к заключению, что wp(S, Q) ⇒ wp(S, Q or R) для всех состояний и аналогично wp(S, R) ⇒ wp(S, Q or R) для всех состояний Но, согласно исчислению высказываний, из A ⇒ C и B ⇒ C можно заключить, что (A or B) ⇒ C, и этим доказана справедливость соотношения (8). Вообще говоря, следование в обратном направле- нии не имеет места. Так про женщину, которая ждет ребенка, неверно утверждение, что она родит обязательно сына и неверно утверждение, что она родит обязательно дочь; однако с абсолютной уверенностью можно утверждать, что она родит сына или дочь. Впрочем, для детерминированных конструкций справедливо следующее, более сильное свойство. Свойство 4’. Для любой детерминированной конструкции S и любых постусловий Q и R справед- ливо (wp(S, Q) or wp(S, R)) ⇒ wp(S, Q or R) 18 Э. Дейкстра. ”Дисциплина программирования” Нам нужно показать, что следование выполняется и в левую сторону. Рассмотрим какое-то на- чальное состояние, удовлетворяющее wp(S, Q or R), этому начальному состоянию соответствует един- ственное конечное состояние, удовлетворяющее либо Q, либо R, либо обоим условиям; следователь- но, данное начальное состояние должно удовлетворять либо wp(S, Q), либо wp(S, R), либо обоим усло- виям соответственно, т. е. он должно удовлетворять (wp(S, Q) or wp(S, R)). И этим доказано свойство 4’. В этой книге я буду — и это может оказаться одной из ее отличительных особенностей — рассмат- ривать недетерминированность как правило, а детерминированность как исключение: детерминиро- ванная машина будет рассматриваться как частный случай недетерминированной, как конструкция, для которой справедливо свойство 4’ а не только более слабое свойство 4. Такое решение отражает коренное изменение в моем мировоззрении. В 1958 г. я был одним из первых, кто разрабатывал ба- зовое программное обеспечение для машины с прерываниями ввода-вывода, и невоспроизводимость поведения такой во всех отношениях недетерминированной машины явилась горестным обстоятель- ством. Когда впервые была предложена идея прерываний ввода-вывода, меня настолько пугала сама мысль о необходимости разрабатывать надежное программное обеспечение для такого неукротимого зверя, что я оттягивал принятие решения о допущении таких прерываний по крайней мере в тече- ние трех месяцев. И даже после того, как я сдался (мое сопротивление сломили лестью), чувствовал я себя весьма неуютно: ведь ошибка в программе способна вызвать несуразное поведение системы, столь сходное с невоспроизводимым машинным сбоем. Кроме того,— и это в то время, когда для де- терминированных машин мы все еще полагались на "отладку",— с самого начала было совершенно очевидно, что тестирование программ оказывалось теперь совсем непригодным средством для дости- жения должного уровня надежности. В течение многих лет впоследствии я относился к невоспроизводимости поведения недетерми- нированной машины как к добавочному осложнению, которого следует избегать любыми способами. Прерывания были для меня не чем иным, как злыми кознями инженеров по аппаратуре против бедных разработчиков программного обеспечения. Из этого моего страха родилась дисциплина "гар- монически взаимодействующих последовательных процессов". Несмотря на ее успех, мои опасения сохранялись, поскольку наши решения — хоть бы и с доказанной правильностью — представлялись частными решениями проблемы "укрощения" (именно так мы это воспринимали!) конкретных видов недетерминированности. Основанием для моего страха было отсутствие общей методологии. С тех пор два обстоятельства изменили картину. Первое возникло с пониманием того, что даже в случае полностью детерминированных машин полезность тестирования программ оказывается со- мнительной. Как я уже много paз говорил и во многих местах писал, тестирование программы может вполне эффективно служить для демонстрации наличия в ней ошибок, но, к сожалению, непригодно для доказательства их отсутствия. Другим прояснившимся тем временем обстоятельством явилось обнаружение необходимости того, чтобы всякая дисциплина проектирования должным образом учи- тывала тот факт, что само проектирование конструкции, предназначенной для какой-то цели, тоже должно быть целенаправленной деятельностью. В нашем конкретном случае это означает естествен- ность предположения, что отправной точкой для проектных рассмотрений будет служить заданное постусловие. В каком-то смысле мы будем "работать вспять". Действуя так, мы обнаружим, что весь- ма существенным оказывается следование из свойства 4, тогда как от равенства из свойства 4’ мы получим очень мало пользы. Как только мы разработали математический аппарат, позволяющий проектировать недетерми- нированные конструкции, достигающие цели, недетерминированная машина перестает нас пугать. Напротив! Мы научимся даже ценить ее как важную степень на пути разработки проекта в конечном итоге полностью детерминированной конструкции. (Последующая часть этой главы может быть пропущена при первом чтении.) Ранее мы догово- рились, что представляем функционирование конструкции S достаточно хорошо, если только знаем, как соответствующий ей преобразователь предикатов wp(S, R) действует над любым постусловием R. Если нам известно также, что данная конструкция детерминирована, то знание этого преобразовате- ля предикатов полностью определяет возможное поведение конструкции. Для детерминированной конструкции S и некоторого постусловия R всякое начальное состояние попадает в одно из трех непе- ресекающихся множеств в соответствии со следующими взаимно исключающими возможностями: (а) Запуск конструкции S приведет к конечному состоянию, удовлетворяющему R. (б) Запуск конструкции S приведет к конечному состоянию, удовлетворяющему non R. (в) Запуск конструкции S не приведет к какому бы то ни было конечному состоянию, т. е. работа не сможет завершиться правильным образом. Э. Дейкстра. ”Дисциплина программирования” 19 Первое множество характеризуется выражением wp(S, R), второе множество — выражением wp(S, non R), их объединение — выражением (wp(S, R) or wp(S, non R)) = wp(S, R or non R) = wp(S, T ) а следовательно, третье множество характеризуется выражением non wp(S, T ). Труднее дать полную семантическую характеристику недетерминированной системы. По отно- шению к любому заданному постусловню R мы снова имеем три возможных типа событий, как пе- речислено выше в пунктах (а), (б) и (в). Однако в случаe недетерминированной системы одно и то же начальное состояние не обязательно приводит к единственному событию, которое по определению относилось бы к одному из трех взаимно исключающих типов; для любого начального состояния возможные события могут теперь относиться к одному, двум или даже ко всем трем типам. Чтобы описывать такие ситуации, мы можем использовать понятие "свободного предусловия". Ранее мы рассмотривали такие предусловия, при которых гарантировалась достижимость "правиль- ного результата", т. е. конечного состояния, удовлетворяющего R. Свободное предусловие является более слабым: оно гарантирует только, что система не выдаст неправильного результата, т. е. не до- стигнет такого конечного состояння, которое не удовлетворяло бы R, однако не исключается возмож- ность незавершения работы системы. Аналогично и для свободных предусловий мы можем ввести понятие "слабейшего свободного предусловия"; обозначим его через wlp(S, R), При этом пространство начальных состояний подразделяется в принципе на семь взаимно непересекающихся областей, ни одна из которых не обязана быть пустой. (Их семь, потому что из трех объектов можно сделать семь непустых выборок.) Все они легко характеризуются тремя предикатами: wlp(S, R), wlp(S, non R) и wp(S, T ). (а) wp(S, R) = (wlp(S, R) and wp(S, T )) Запуск обеспечит истинность R. (б) wp(S, non R) = (wlp(S, non R) and wp(S, T )) Запуск обеспечит истинность non R. (в) wlp(S, F ) = (wlp(S, R) and wlp(S, non R)) Запуск не сможет привести к правильно завершаемой работе (аб) wp(S, T ) and non wlp(S, R) and non wlp(S, non R) Запуск приведет к завершаемой работе, но по начальному стоянию нельзя определить, будет ли конечное состояние удовлетворять условию R или нет. (ав) wlp(S, R) and non wp(S, T ) Если запуск приводит к какому-то конечному состоянию, такое конечное состояние будет удовлетво- рять R, но по начальному состоянию нельзя определить, завершится ли работа системы. (бв) wlp(S, non R) and non wp(S, T ) Если запуск приводит к какому-то конечному состоянию, такое конечное состояние не будет удовле- творять R, но по начальному состоянию нельзя определить, завершится ли работа системы. (абв) non(wlp(S, R) or wlp(S, non R) or wp(S, T ) По начальному состоянию нельзя определить, приведет ли запуск к завершаемой работе, а в случае завершаемости нельзя определить, будет ли удовлетворяться условие R. Последние четыре возможности существуют только для недетермированных машин. Из определения wlp(S, R) следует, что wlp(S, T ) = T Ясно также, что (wlp(S, F ) and wp(S, T )) = F 20 Э. Дейкстра. ”Дисциплина программирования” Если бы было не так, то существовало бы начальное состояние, для которого можно было бы гарантировать и завершимость, и незавершимость работы. На рис. 3.1 дано графическое //рис.31 представление пространства состояний,причем внутренние части прямоугольников удовлетворяют wlp(S, R), wlp(S, non R) и wp(S, T ) соответственно. Этот анализ приведен для полноты, а также потому, что на практике понятие свободного преду- словия оказывается весьма полезным. Если, например, кто-то реализует язык программирования, то он не станет доказывать, что при этой реализации любая правильная программа выполняется пра- вильно. Он был бы удовлетворен и счастлив, если бы твердо знал, что никакая правильная программа не будет выполнена правильно без соответствующего предупреждения,— разумеется, при условии, что класс программ, которые на самом деле будут выполняться правильно, достаточно велик для того, чтобы эта реализация представляла какой-то интерес. Однако пока мы не будем рассматривать понятие свободного предусловия, а сосредоточим свое внимание на способе характеристики тех начальных состояний, которые гарантируют получение правильного результата. Когда такой способ будет разработан, мы посмотрим, как можно его видо- изменить таким образом, чтобы это позволило нам рассуждать о свободных предусловиях в той мере, в которой они нас интересуют. Э. Дейкстра. ”Дисциплина программирования” 21 4 СЕМАНТИЧЕСКАЯ ХАРАКТЕРИСТИКА ЯЗЫКОВ ПРОГРАММИРОВАНИЯ В предыдущей главе мы выдвинули тезис, что знаем семантику конструкции S достаточно хо- рошо, если знаем ее "преобразователь предикатов", т. е. правило, указывающее нам, как вывести по любому постусловию R соответствующее слабейшее предусловие (которое мы обозначили через wp(S, R)), характеризующее те начальные состояния, при которых запуск приведет к событию пра- вильного завершения, причем система останется в конечном состоянии, удовлетворяющем постусло- вию R. Вопрос в том, как выводить wp(S, R) для заданных S и R. Оставим пока вопрос об одиночной конкретной конструкции S. Программа, написанная на хоро- шо определенном языке программирования, может рассматриваться как некая конструкция, такая конструкция, которую мы знаем достаточно хорошо, если знаем соответствующий преобразователь предикатов однако язык программирования полезен только при том условии, что его можно при- менять для записи многих различных программ, и для всех этих программ нам желательно знать соответствующие им преобразователи предикатов. Каждая такая программа задается своим текстом на хорошо определенном языке программиро- вания, и поэтому ее текст должен служить для нас отправной точкой. Но теперь перед нами неожидан- но открываются два совершенно различных назначения такого текста программы. С одной стороны, текст программы предназначен для машинной интерпретации, если мы хотим, чтобы она могла вы- полняться автоматически, если мы хотим, чтобы по ней для нас был произведен какой-либо конкрет- ный расчет. С другой стороны, желательно, чтобы текст программы говорил нам о том, как строить соответствующий преобразователь предикатов, как производить преобразование предикатов, чтобы выводить предусловие wp(S, R) для любого данного постусловия R, которое нас почему-либо заинте- ресовало. Это замечание позволяет понять, что подразумевается под "хорошо определенным языком программирования" с нашей точки зрения. Когда семантика конкретной конструкции (или програм- мы) задается ее преобразователем предикатов, мы рассматриваем семантическую характеристику языка программирования как набор правил, которые позволяют любой программе, написанной па этом языке, поставить в соответствие преобразователь предикатов. С такой точки зрения мы можем рассматривать программу как "код" для соответствующего преобразователя предикатов. При желании можно подойти к проблеме проектирования языка программирования с такой пози- ции. Можно руководствоваться (довольно формально) тем, что правила построения преобразователей предикатов должны быть такими, чтобы, применяя их, нельзя было построить ничего другого, кро- ме как преобразователя предикатов, обладающего свойствами 1–4 из предыдущей главы. В самом деле, если правила не дают такой гарантии, то это означает, что вы деформируете предикаты таким образом, что они уже не могут интерпретироваться как постусловия и соответствующие слабейшне предусловия. Сразу напрашиваются два примера весьма простых преобразователей предикатов, которые обла- дают требуемыми свойствами. Начнем с тождественного преобразования, т. е, с конструкции S, такой, что для любого постусло- вия R мы имеем wp(S, R) = R. Эту конструкцию знают и любят все программисты: она известна им под названием "пустой onepaтор", и в своих программах они часто используют ее, оставляя пропуск в том месте текста, где синтаксически требуется какой-то оператор. Это не слишком похвальный прием (компилятор должен знать, что он "видит" этот оператор, на том основании, что он ничего не ви- дит, и поэтому мы дадим этой конструкции наименование, скажем, "пропустить". Итак, семантика оператора "пропустить" определяется следующим образом: wp(пропустить, R) = R для любого постусловия R (Как и все, я буду пользоваться термином "оператор", поскольку он прочно вошел в жаргон. Когда люди сообразили, что "команда" могла бы оказаться более подходящим термином, было уже слишком поздно 1 .) Замечанue. Тем, кто считает расточительством символов введение явного имени "пропустить" для пустого оператора, когда "пусто" столь красноречиво выражает его семантику, следует осознать, что десятичная система счисления оказалась возможной только благодаря введению символа "0" для понятия "ничто". (Конец замечания.) Прежде чем продолжить наши рассуждения, мне хотелось бы не упустить возможность отметить, что тем временем мы уже определили некий язык программирования. Остается добавить только одно: 1 По традиции мы переводим английский термин "statement" (утверждение, предложение) тер- мином "оператор", введенным в программирование А. А. Ляпуновым, и таким образом, русский читатель оказывается в более выгодном положении, чем английский.—Прим. ред. |