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

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

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

v.

Получаем правило вывода

(Y = e) = > B(Y)

------------------

B( v --> Y )

где под горизонтальной чертой изображен результат подстановки знака v в

утверждение B вместо всех вхождений знака Y.

Итак, преодоление присваивания состоит из двух шагов, первый из которых

содержательный (творческий), а второй - формальный. На первом нужно найти

инвариант B, характеризующий старое значение выражения e (причем в него не

должен входить знак v !). На втором шаге можно формально применить правило

вывода постусловия.

Замечание. Для предусловий, не содержащих v, тривиальное правило

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

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

таких свойств программ, на которые преодолеваемые операторы не могут

повлиять в принципе. Однако интереснее, конечно, правило преодоления,

существенно учитывающее операционную семантику преодолеваемого оператора.

Такими правилами мы и занимаемся.

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

нашей программе-примеру, стараясь преодолеть оператор (1-2) и получить

"интуитивно" написанное нами постусловие q(2) теперь уже формально.

Во-первых, нужно подобрать подходящее B. Как уже было объяснено, это

задача творческая. Зная q(2), можно догадаться, что B должно иметь вид

{ n >= 1 & Y = M[1] }.

Замечание. Вот так знание желательного постусловия (по существу, знание

цели выполняемых действий) помогает формально преодолевать конструкты

программы.

Нам нужно вывести из q(1) обычными логическими средствами предусловие

для преодоления оператора (1-2). Другими словами, подготовить предусловие

для формального преодоления оператора.

Предусловие должно иметь вид

(Y = M[1]) ==> (n >= 1 & Y = M[1])

Оно очевидно следует из n >= 1. Формально следует применить схему

аксиом

(A => ( C => A & C )

и правило вывода модус поненс

A, A => B

---------

B

Подставляя вместо A утверждение (n >= 1), а вместо C - утверждение

(Y=M[1]), получаем нужное предусловие. Итак, все готово для формального

преодоления фрагмента (1-2) с помощью правила преодоления присваивания.

Совершенно аналогично нетрудно преодолеть и фрагмент (2-3), получив

q(3) :: (n >= 1 & x = M[1] & i = 1).

Замечание. Нетривиальность первого из этапов преодоления оператора

присваивания подчеркивает принципиальное отличие дедуктивной семантики от

операционной. Дедуктиная семантика не предписывает, а разрешает. Она

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

связь предусловия с постусловием. Зато она позволяет преодолевать один и тот

же оператор по-разному, выводя разные постусловия в зависимости от

потребностей того, кто выясняет (или доказывает) свойства программы. Можете

ли Вы привести пример постусловия для (2-3), отличного от q(3)?

Перепишем наше правило преодоления присваивания, обозначив через L

предусловие, а через R - постусловие.

L :: (Y = e ) => B(Y)

П(1) ---------------------

R :: B( v --> Y) .

Чтобы преодолеть конструкт (3-8), нужно запастись терпением и

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

языка Д.

Дедуктивная семантика развилки. Рассмотрим развилку S вида

"if"

P1 --> S1 ,

...

...

Pn --> Sn

"fi" .

Наша задача - формализовать для нее правила преодоления. Вспомним, что

по смыслу (операционной семантике) развилки каждая ее i-я ветвь Si

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

завершение Si означает завершение всей развилки S. Так как по определению

постусловия оно должно быть истинным после выполнения любой ветви, получаем

следующее естественное правило преодоления, сводящее преодоление S к

преодолению ее ветвей.

Ak : {L & Pk} Sk {R}

(П2) --------------------

R

где L и R соответственно пред- и постусловия для S.

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

случаев, подбирая такое R, чтобы оно было истинным в каждом из них. Очень

часто R представляет собой просто дизъюнкцию постусловий R1v...vRn для

операторов S1,...,Sn соответственно. Подчеркнем, что преодоление развилки

невозможно, если не выполнено ни одно условие Ri.

Дедуктивная семантика точки. Поскольку наша цель - научиться формально

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

семантикой, то естественно считать допустимой эамену утверждения,

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

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

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

логическое правило вывода - правилом преодоления пустого фрагмента.

Применение таких правил очень важно - с их помощью готовят преодоление

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

преодолении фрагмента (1-2). Таким образом, дедуктивная семантика точки

совпадает с дедуктивной семантикой пустого фрагмента. Такова же и

дедуктивная семантика оператора "null".

Дедуктивная семантика цикла. Рассмотрим цикл вида

"do"

P1 --> S1,

...

...

Pn --> Sn

"od" .

Наша задача - сформулировать правило его преодоления. Вспомним

операционную семантику этого оператора. Он завершает исполнение тогда и

только тогда, когда истинно "not" P1 & ... & "not" Pn. Обозначим эту

конъюнкцию отрицаний через P и немного порассуждаем о природе циклов.

Циклы - важнейшее средство для описания потенциально неограниченной

совокупнисти действий ограниченными по длине предписаниями. Таким средством

удается пользоваться в содержательных задачах только за счет того, что у

всех повторений цикла обнаруживается некоторое общее свойство, "инвариант

цикла", не меняющийся от повторения к повторению.

В языке Д выполнение циклов состоит только из повторений тела цикла,

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

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

Обозначим инвариант цикла через I. Естественно, у одного цикла много

различных инвариантов (почему?). Тем не менее основную идею цикла,

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

достаточно полным инвариантом I и условием завершения P. Условие P отражает

достижение цели цикла, а конъюнкция I & P - свойство состояния программы,

достигнутого к моменту завершения цикла. Значит, это и есть постусловие для

цикла S. А предусловием служит, конечно, инвариант I - ведь он потому так

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

непосредственно после каждого исполнения тела цикла. Осталось выразить

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

I

(П3) -------

I & P .

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

отражена способность утверждения I служить инвариантом цикла. Нужно еще явно

потребовать его истинности после каждого исполнения тела (или, что то же

самое, после исполнения каждой ветви). Получаем следующее развернутое

правило преодоления

Ak : {I & Pk} Sk {I}

(П4) --------------------

I & P .

Другими словами, если утверждение I служит инвариантом цикла, т.е. для

каждого Pk сохраняется при выполнении k-й ветви цикла, то результатом

преодоления всего цикла может служить постусловие I & P.

Скоро мы продолжим движение по нашей программе с использованием

инвариантов цикла. Но прежде завершим построение дедуктивной семантики языка

Д.

От точечных условий к тройкам. Нетрудно заметить, что как в правиле

(П2), так и в (П4) предусловиями служат не точечные условия, а тройки Хоара.

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

Оно довольно очевидно. В сущности именно его мы имели в виду, объясняя саму

идею преодоления фрагментов. Зафиксируем некоторый фрагмент Ф и обозначим

через L(Ф) некоторое точечное условие для его левого конца, а через R(Ф) -

некоторое точечное условие для его правого конца. Через "!==>" обозначим

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

L(Ф) !==> R(Ф)

(П5) --------------

{L} Ф {R} .

Замечание. Может показаться, что это правило не совсем естественное и

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

заниматься любыми фрагментами. Действительно, достаточно применять это

правило только для присваиваний, ветвлений, циклов и последовательностей

операторов. Но верно оно и в том общем виде, в котором приведено (почему?).

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

предшествовала точке привязки R. Нужна именно выводимость в нашем исчислении

(почему?).

Итак, мы завершили построение исчисления, фиксирующего дедуктивную

семантику языка Д.

15.2.7. Применение дедуктивной семантики

Теперь мы полностью готовы к дальнейшему движению по нашей программе-

примеру. Предстоит преодолеть цикл (3-11) из п.15.2.3, исходя из предусловия

q(3) и имея целью утверждение q(11). Подчеркнем в очередной раз, как важно

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

получив постусловие n >= 1, но нам-то хотелось бы q(11) ! ).

Правило преодоления цикла требует инварианта. Но нам годится не любой

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

q(11). Интуитивно ясно, что он должен быть в некотором смысле оптимальным -

с одной стороны, выводимым из q(3), а с другой - позволяющим вывести q(11).

Обычная эвристика при поисках такого инварианта - постараться полностью

выразить в нем основную содержательную идею рассматриваемого цикла.

Замечание. Важно понимать, что разумные циклы преобразуют хотя бы

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

(принимающих, естественно, разные значения в процессе выполнения цикла).

Однако должно оставаться неизменным фиксируемое инвариатом соотношение между

этими значениями.

Внимательно изучая цикл (3-11) из п.15.2.3, можно уловить его идею -

при каждом повторении поддерживать x равным max(M,i), чтобы при i = n

получить q(11). Выразим этот замысел формально

I1 :: (x = max(M,i)

и попытаемся с помощью такого I1 преодолеть наш цикл.

Замечание. "Вылавливать" идеи циклов из написанных программ - довольно

неблагодарная работа. Правильнее было бы формулировать инварианты при

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

заготовленными инвариантами. Мы лишены возможности так действовать, потому

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

недавно. Однако и у нашего пути есть некоторые преимущества. По крайней мере

есть надежда почуствовать сущность оптимального инварианта.

Предстоит решить три задачи:

а. Доказать, что I1 - действительно инвариант цикла (3-11).

б. Доказать, что условие q(11) выводимо с помощью I1.

в. Доказать, что из q(3) логически следует I1.

Естественно сначала заняться двумя последними задачами, так как наша

цель - подобрать оптимальный инвариант. Если с помощью I1 нельзя, например,

вывести q(11), то им вообще незачем заниматься. Так как задача (в)

тривиальна при i = 1, займемся задачей (б).

Замечание. На самом деле задача (в) тривиальна лишь при условии, что

можно пользоваться формальным определением функции max (точнее, определяющей

эту функцию системой соотношений-аксиом). Например, такими соотношениями:

Ek : (k >= 1) & (k <= i) & M[k] = max(M,i) .

Ak : (k >= 1) & (k <= i) => M[k] <= max(M,i) .

При i = 1 отсюда следует M[1] = max(M,1). Так что I1 превращается в

(x = M[1])

т.е. просто в одну из конъюнкций q(3).

По сути это замечание привлекает внимание к факту, что при

доказательстве правильности программ методом Хоара приходится все

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

порядка и непосредственно применять эти (довольно громоздкие) описания в

процессе преодоления конструктов. Сравните с методом Бэкуса.

Первая попытка решить задачу б. Итак, допустим, что I1 - инвариант

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

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