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. Эту конструкцию знают и любят все программисты: она известна им под названием "пустой оператор", и в своих программах они часто используют ее, оставляя пропуск в том месте текста, где синтаксически требуется какой-то оператор. Это не слишком похвальный прием (компилятор должен знать, что он "видит" этот оператор, на том основании, что он ничего не видит, и поэтому мы дадим этой конструкции наименование, скажем, "
пропустить". Итак, семантика оператора "пропустить" определяется следующим образом:
(Как и все, я буду пользоваться термином "оператор", поскольку он прочно вошел в жаргон. Когда люди сообразили, что "команда" могла бы оказаться более подходящим термином, было уже слишком поздно
1.)Замечание.
Тем, кто считает расточительством символов введение явного имени "пропустить" для пустого оператора, когда "пусто" столь красноречиво выражает его семантику, следует осознать, что десятичная система счисления оказалась возможной только благодаря введению символа "О" для понятия "ничто". (Конец замечания.)Прежде чем продолжить наши рассуждения, мне хотелось бы не упустить возможность отметить, что тем временем мы уже определили некий язык программирования. Остается добавить только одно:
это однооператорпый язык, в котором можно описать только одну конструкцию, причем единственное, что способна сделать для нас данная конструкция, это "оставить все, как есть" (или "ничего не делать", но такое негативное употребление языка представляет опасность, см. следующий абзац).
Другой простой преобразователь предикатов приводит к постоянному слабейшему предусловию, которое вовсе не зависит от постусловия R. Мы имеем два предиката-константы,
Т и F. Конструкция S, для которой wp(S', R) = Т при всех R, не может существовать, потому что она нарушила бы закон исключенного чуда. Однако конструкция S, для которой wp(S', R) = F при всех R, обладает преобразователем предикатов, удовлетворяющим всем необходимым свойствам. Этому оператору мы тоже присвоим имя, назовем его "отказать". Итак, семантика оператора "отказать" задается следующим образом:
Этот оператор не может даже "ничего не делать" в смысле "оставить все, как есть"; он вообще ни на что не способен. Если мы полагаем R =
Т, т. е. не накладываем на конечное состояние никаких дополнительных требований, кроме самого факта его существования, даже тогда не найдется соответствующего начального состояния. Если запустить конструкцию по имени "отказать", она не сможет достичь конечного состояния: сама попытка ее запуска является гарантией неудачи. (Нас не должно занимать теперь (а также и впоследствии) то, что позднее мы введем структуру операторов, в которой содержатся как частные случаи семантические эквиваленты для "пропустить" и "отказать".)Теперь мы располагаем неким (все еще весьма зачаточным) двухоператорным языком программирования, в котором можем описать две конструкции; одна из них ничего не делает, а вторая всегда терпит неудачу. Со времени опубликования знаменитого "Собщения об алгоритмическом языке АЛГОЛ 60" в 1960 г. никакой уважающий себя ученый, занимающийся программированием, не позволит себе обойтись на этом этапе без формального определения синтаксиса столь далеко продвинутого языка программирования в системе обозначений, называемой "НФБ" (сокращение от "Нормальная форма Бэкуса"), а именно:
(Читается так: "Элемент синтаксической категории, именуемой "оператор" (именно это обозначают забавные скобки "<" и ">"), определяется как (это обозначает знак "::=") "
пропустить" или (это обозначает вертикальная черта "|") "отказать". Колоссально! Но не беспокойтесь; более впечатляющие применения НФБ в качестве способа записи последуют в надлежащее время.)Один класс безусловно более интересных преобразователей предикатов основывается на подстановке, т. е. на замене всех вхождений некоей переменной в формальном выражении для постусловия
R на (одно и то же) "что-нибудь другое". Если в предикате R все вхождения переменной х заменяются некоторым выражением (Е), то мы обозначаем результат этого преобразования через re^x- Теперь мы можем рассмотреть для заданных х и Е такую конструкцию, чтобы для любых постусловий R получалось wp(S', R) = re^x ; здесь х — "координатная переменная" нашего пространства состояний, а Е — выражение соответствующего типа.Замечание.
Такое преобразование путем подстановки удовлетворяет свойствам 1—4 из предыдущей главы. Мы не станем пытаться демонстрировать это и предоставим самому читателю решать в зависимости от своего вкуса, будет ли он относиться к этому как к тривиальному или же как к глубокому математическому результату. (Конец замечания.)Таким способом вводится целый класс преобразователей предикатов, целый класс конструкций. Они обозначаются оператором, который называется "оператор присваивания"; такой оператор должен определять три вещи:
1) наименование переменной, подлежащей замене;
2) тот факт, что правило, соответствующее преобразованию предикатов, есть подстановка;
3) выражение, которым должно заменяться всякое вхождение этой переменной в постусловии. Если переменная
х должна быть заменена выражением (Е) то обычная запись такого операторавыглядит следующим образом:
х := Е
(где так называемый знак присваивания ":=" следует читать как "становится"). Сказанное можно суммировать, определив
wp("a; :=
Е", R) = re^x Для любого постусловия RПри желании это можно рассматривать как семантическое определение оператора присваивания для любой координатной переменной
х и любого выражения Е соответствующего типа. Наслаждаясь,Э. Дейкстра. "Дисциплина программирования"
23по нашему обыкновению, употреблением НФБ, мы можем расширить наш формальный синтаксис, чтобы он читался так:
причем последнюю строчку следует читать так: "Элемент синтаксической категории, именуемой "оператор присваивания", определяется как элемент синтаксической категории, именуемой "переменная" , за которым следуют сначала знак присваивания " :=", а затем элемент синтаксической категории, именуемой "выражение". Перед тем как продолжить рассуждение, представляется разумным убедиться в том, что этим формальным описанием оператора присваивания в самом деле охватывается наше интуитивное понимание оператора присваивания — если оно у нас есть! Рассмотрим пространство состояний с двумя целыми координатными переменными "а" и "Ь". Тогда
Читать дальше
