В.Ш. Кауфман - Языки программирования - концепции и принципы (1990) (1160787), страница 57

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 57)

AA IP * A distl * distr * (t1 * 1,2)).

----- Af ------ ------- h --------

Tак как A (A IP * distl) = AA IP * A distl [по закону 7 из

15.1.2.], то R'' имеет вид

appendl * (f * g , A f * h)

для указанных под определением R''функций f, g и h.

Поэтому по закону 5 из 15.1.2.

R'' = A f * appendl * (g, h) =

= A f * appendl * ((1 * 1 , 2) , distr * (t1 * 1 , 2))

что по закону 6 дает

A f * distr

т.е. ММ'. Теорема доказана.

Каждый из трех использованных в доказательстве общих законов очевиден

(следует непосредственно из определения соответствующих функций) и может

быть обоснован аналогично закону 6.

15.2. Доказательное программирование методом Хоара

На примере метода Бэкуса видно, как подход к доказательному

программированию связан со свойствами ЯП, к которому этот метод применяется

(модель Б специально строилась так, чтобы были справедливы достаточно

простые законы алгебры программ). Метод Хоара, к изложению которого мы

приступаем, также ориентирован на определенный класс ЯП.

Эти ЯП ближе к традиционным (во всяком случае в них имеются переменные

и присваивания). Характерное ограничение состоит в том, что динамическая

структура программы в них должна быть хорошо согласована со статической ее

структурой. Другими словами, составить представление о процессе выполнения

программы должно быть относительно легко по ее тексту.

Иначе о том же можно сказать так: в этих ЯП по структуре знака

относительно легко судить о структуре денотата.

Указанное согласование и позволяет реализовать основную идею Тони Хоара

- ввести так называемую дедуктивную семантику языка, связывающую программные

конструкты непосредственно с утверждениями о значениях программных

переменных. При этом математической моделью программы служит так называемая

"аннотированная программа", к которой применимы правила преобразования

(правила вывода), представляющие, с одной стороны, ее (дедуктивную)

семантику, а с другой стороны, математическую модель внешнего мира.

Допустимы, конечно, и иные содержательные истолкования метода Хоара.

Например, сами утверждения о свойствах программы, входящие в аннотированную

программу, можно считать элементами модели внешнего для программы мира.

Существенны не эти различия, а факт, что в методе Хоара, как и в любом

методе доказательного программирования, необходимо формально описывать и

программу, и требования к ней, и допустимые их связи и преобразования.

Рассмотрим метод Хоара на примере конкретного ЯП и конкретной программы

в этом ЯП. Поскольку для нас важны ключевые идеи, а не точное следование

классическим текстам, будем вносить в традиционное изложение метода

изменения, по нашему мнению облегчающие понимание сути дела.

15.2.3. Модель Д

В качестве представителя рассматриваемого класса ЯП рассмотрим модель Д

очень простого ЯП, который также назовем языком Д. Он очень похож на язык,

использованный Дейкстрой в [24]. Начнем с описания синтаксиса языка Д с

помощью несколько модифицированной БНФ. И сам синтаксис, и применяемую

модификацию БНФ (она соответствует предложениям Вирта и принята в качестве

английского национального стандарта) удобно объяснять в процессе пошаговой

детализации исходного синтаксического понятия "программа". На каждом шаге

детализации при этом указываются все допустимые конкретизации промежуточных

синтаксических понятий (абстракций). В зависимости от интерпретации

применяемые при этом правила конкретизации можно считать или соотношениями,

связывающими классы текстов (так называемые формальные языки), или правила

вывода в некоторой порождающей системе (а именно, в контекстно-свободной

грамматике). Ниже выписаны 16 шагов такой детализации (т.е. 16 правил

модифицированной БНФ).

Синтаксис языка Д.

программа = 'begin' { объявление ';' }{ оператор ';' } 'end'.

объявление = ( 'var' ! 'arr' ) имя { ',' имя } .

оператор = присваивание ! развилка ! цикл ! 'null' .

присваивание = переменная ':=' выражение .

переменная = имя [индекс] .

индекс = '[' выражение ']' .

выражение = переменная ! число ! функция .

функция = имя '(' выражение { ',' выражение } ')' .

развилка = 'if' { вариант } 'fi' .

цикл = 'do' { вариант } 'od' .

вариант = условие '-->' { оператор ';' } .

условие = выражение (< ! <= ! = ! /= ! >= ! > ) выражение .

имя = буква { буква ! цифра } .

число = цифра { цифра } .

буква = 'a' ! 'b' ! ... ! 'z' .

цифра = '0' ! '1' ! ... ! '9' .

Отличия от оригинальной БНФ сводятся, во-первых, к тому, что

выделяются не названия синтаксических понятий (метасимволы), а символы так

называемого терминального алфавита (т.е. алфавита, из символов которого

строятся программы в описываемом языке). В языке Д терминальный алфавит

состоит из букв, цифр и символов 'begin', 'end', 'var', 'arr', 'do', 'od',

'if', 'fi', 'null', и некоторых других (скобок, знаков отношений и т.п.). В

неясных случаях для выделения терминальных символов применяется апостроф.

Во-вторых, применяются круглые, квадратные и фигурные скобки. Круглые -

чтобы сгруппировать несколько вариантов конкретизации понятия (несколько

альтернатив). Квадратные - чтобы указать на возможность опускать их

содержимое. Фигурные - чтобы указать на возможность выписывать их содержимое

нуль и более раз подряд в процессе пошаговой детализации (или, как говорят,

порождения) конкретной программы.

Некоторый текст признается допустимой программой на языке Д тогда и

только тогда, когда его можно получить последовательной конкретизацией (т.е.

породить) по указанным 16 правилам из исходной абстракции "программа". Такой

текст называется выводимым из метасимвола "программа".

Например, текст

'begin' 'var' x, i, n ;

x := M[1] ; i := 1 ;

'do' i < n --> i := plus(i,1) ;

'if' M[i] > x --> x := M[i] ;

M[i] <= x --> 'null' ; 'fi' ;

'od' ;

'end'

допустим в языке Д, а если вместо 'plus(i,1) написать "i+1", то получится

недопустимый текст (так как "выражение" может быть только "переменной",

"числом" или "функцией"). Однако мы позволим себе для наглядности писать

"i+1".

Семантика языка Д. Поясненим только смысл развилки и цикла. Смысл

остальных конструктов традиционен. Для наших целей достаточно интуитивного

представления о нем.

Начнем с так называемой операционной семантики развилки и цикла.

Другими словами, поясним, как эти конструкты выполняются.

Назовем состоянием некоторое отображение переменных программы в их

значения. Это отображение частичное, потому что значения некоторых

переменных могут быть неопределенными. Вот пример состояния выписанной выше

программы (Она вычисляет максимум M[i] )

< n --> 5, M --> (2,5,6,8,1), x --> 2, i --> 1 > .

Рассмотрим развилку S вида

'if'

P1 --> S1 ,

...

Pn --> Sn

'fi' .

Полезно учитывать, что смысл конструктов языка Д специально подобран

так, чтобы было легче доказывать свойства написанных на нем программ. Как

доказывать, рассмотрим в следующем пункте, а пока объясним семантику

развилки S.

Пусть S начинает выполняться в некотором состоянии W. Сначала в

состоянии W асинхронно (независимо, возможно и параллельно) вычисляются все

Pi. Каждое из них либо нормально завершается и дает истину или ложь, либо

завершается отказом (в частности, зацикливанием). Если хотя бы одно Pi дает

отказ, то S завершается отказом. Если все Pi нормально завершаются

(состояние W при этом не меняется!), то случайным образом выбирается Si0 -

одно из тех и только тех Si, для которых Pi истинно. Результат выполнения

этого Si0 в состоянии W - это и есть результат выполнения всей развилки S.

Если же все Pi дают ложь, то S завершается отказом.

Рассмотрим цикл S вида

'do'

P1 --> S1 ,

...

Pn --> Sn

'od' .

Выполнение цикла отличается от развилки тем, что если все Pi дают ложь,

то S нормально завершается с состоянием W (т.е. его действие в этом случае

равносильно пустому оператору). Когда же выбирается Si0, то после его

нормального завершения в некотором состоянии Wi0 цикл S снова выполняется в

состоянии Wi0. Другими словами, он выполняется до тех пор, пока все Pi не

дадут ложь или не возникнет отказ (в последнем случае и весь S завершится

отказом).

Вот и все, что нужно знать об (операционной) семантике языка Д, чтобы

воспринимать еще один подход к доказательному программированию.

Как видите, семантика языка Д очень "однородная", она симметрична

относительно различных вариантов составных конструктов. Это помогает

рассуждать о программах, написанных на таком языке.

15.2.4. Дедуктивная семантика

Мы уже не раз упоминали о том, что с одними и теми же текстами

(сообщениями) можно связывать различный смысл в зависимости от роли, которую

они играют при решении конкретных задач. Это справедливо и для текстов

программ, написанных на ЯП. С точки зрения исполнителя, будь в этом качестве

человек или машина, смыслом программы естественно считать предписываемую

этой программой последовательность действий исполнителя. Правила,

сопоставляющие программе последовательность действий (в общем случае - класс

последовательностей, соответствующих классу аргументов) - это

"исполнительская" семантика. Обычно ее называют операционной -

установившийся, но не слишком удачный термин, "калька" английского

operational.

Замечание.. Обычно предполагается, что потенциальный исполнитель

программы цели своих действий не знает и не должен знать. Если считать, что

уровень интеллекта связан со способностью соотносить планируемые

(выполняемые) действия с поставленными целями, то потенциальный исполнитель

программы начисто лишен интеллекта, абсолютно туп. Однако эта тупость

обусловлена такими его потенциальными достоинствами, как универсальность,

определенность и быстродействие. Компьютер способен на все, так как "не

ведает, что творит" и делает, что "прикажут"; ему "не приходит в голову"

действовать по собственной воле, он не тратит ресурсов на оценку разумности

программы, а просто выполняет ее! С такой точки зрения "тупая" операционная

семантика вполне оправдана и весьма полезна - она создает прочную основу для

взаимодействия авторов, пользователей и реализаторов ЯП.

Было время, когда только операционную семантику и связывали с ЯП. Да и

сейчас, когда говорят или пишут о семантике ЯП, чаще всего имеют в виду

именно ее (вспомните известные вам описания Фортрана, Бейсика, Си и др.).

Знакомя с языком Д, мы также начали с его операционной семантики.

Станем на точку зрения пользователя языка. Нормальный пользователь

интеллектом, конечно, обладает и для него естественно соотносить свои

действия со своими целями. Поэтому "исполнительской" семантики ему, как

правило, недостаточно. Ему нужна более "интеллектуальная" семантика, лучше

помогающая судить о той роли, которую программа в состоянии играть при

решении его задач. Операционная семантика обычных ЯП уводит в дебри мелких

действий вместо того, чтобы предоставить интегральную (цельную)

характеристику связи аргументов и результатов программы.

Форм, в которых можно давать такую характеристику, может быть много. С

каждой из них связан свой способ приписывать программе смысл, своя

семантика. Вы уже знакомы с таким способом, когда программе сопоставляется

отображение ее аргументов в результаты - это денотационная семантика. Мы

займемся еще одной, дедуктивной семантикой (иногда ее называют

аксиоматической или логической).

Если операционная семантика предназначена в основном для того, чтобы

четко зафиксировать правила поведения исполнителя (тем самым и выразительные

возможности пользователя), то дедуктивная семантика предназначена в основном

для того, чтобы четко зафиксировать правила поведения пользователя при

доказательстве свойств программ. Наиболее интересное из таких свойств -

свойство давать определенные результаты при определенных аргументах.

Уточним несколько туманный смысл слова "определенный". Как и прежде,

будем называть состоянием программы отображение переменных программы в их

значения. Так что состояние меняется при каждом изменении значения какой-

Характеристики

Список файлов книги