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

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

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

либо переменной.

Говорят, что программа Р частично корректна относительно предусловия Q

и постусловия R, если для всякого начального состояния, удовлетворяющего

условию Q, заключительное состояние удовлетворяет условию R.

Тот факт, что программа Р частично корректна, можно записать с помощью

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

{Q} P {R}

где в скобках явно выписываются соответствующие пред- и постусловия.

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

заключительное состояние - в общем случае возможен отказ или зацикливание.

Свойство полной корректности записывается обычно тройкой Хоара с

квадратными скобками

[Q] P [R]

что означает: "начав с состояния, удовлетворяющего предусловию Q,

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

постусловию R".

Дедуктивная семантика - это правила сопоставления каждой программе

множества ее троек Хоара. Следуя Хоару, эти правила представляют обычно в

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

котором кроме общих аксиом и правил вывода (исчисления предикатов первого

порядка) имеются и правила вывода троек Хоара (свои для каждого ЯП). Тем

самым каждой программе в ЯП ставится в соответствие ее "дедуктивный" смысл -

множество формально выводимых в этом исчислении троек Хоара. Если такая

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

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

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

рассматриваемом ЯП; например, доказательства их частичной или полной

корректности.

15.2.5. Компоненты исчисления Хоара

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

применения дедуктивной семантики ЯП (на примере языка Д и программы

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

рассмотренной с теми же целями в [1].

Во-первых, нужно уметь выражать условия на состояния программы. Для

этой цели нам послужат обычные логические формулы, в которых в качестве

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

Другими словами, условия на состояния мы намерены выражать на

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

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

(свойство ее частичной корректности):

{ n >= 1 }

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

'do' i < n --> i := i + 1 ;

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

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

'od' ;

{ x = max (M,n) } .

Оно говорит о том, что если запустить записанную между пред- и

постусловиями программу при n >= 1, то после ее завершения будет истинным

условие x = max (M,n), т.е. значение переменной x будет равно максимальному

элементу массива M при изменении индекса от 1 до n.

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

свою работу (ведь выписано условие частичной, а не полной корректности!).

Кстати, перед нами пример аннотированной программы, т.е. программы на

"обычном" ЯП, снабженной аннотациями на специальном языке аннотаций. В нашем

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

тройками Хоара и другими полезными дополнениями.

Во-вторых, нужно от свойств одних фрагментов программы уметь переходить

к свойствам других фрагментов (в частности, соседних или вложенных). Ясно,

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

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

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

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

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

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

программирования. Язык Д удовлетворяет этому принципу.

В-третьих, чтобы говорить о свойствах фрагментов программы, нужно уметь

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

программы, но и фрагменты программ. Кроме того, полезно "разметить"

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

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

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

(1) x := M[1] ; (2) i := 1 ; (3)

'do' i < n --> (4) i := i + 1 ; (5)

'if' M[i] > x --> (6) x := M[i] ; (7)

M[i] <= x --> (8) 'null' (9) 'fi' ; (10)

'od' ; (11)

Весь этот фрагмент теперь можно обозначить как Ф(1-11) или даже .

просто (1-11). Условие на состояние программы в точке t обозначим через

q(t). Так что предусловие для Ф(1-11) получит обозначение q(1), а

постусловие q(11). Для обозначения тождества условий будем применять двойное

двоеточие. Так что, например

q(11) :: { x = max(M,n) } .

Наконец, в четвертых (самое важное), для каждого языкового конструкта

нужно сформулировать правила вывода соответствующих троек Хоара. Эти правила

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

для всего ЯП - дедуктивной семантикой ЯП. Вскоре мы построим такую семантику

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

Как уже сказано, для каждого конструкта языка Д нужно сформулировать

правило вывода допустимых троек Хоара. Тройки Хоара абсолютны в том смысле,

что их истинность не зависит от контекста фрагмента, входящего в тройку

(почему?). Однако выводить тройки Хоара удобно с помощью условий,

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

условия обычно относительны в том смысле, что их истинность (и выводимость)

зависят от других точечных условий.

Процесс вывода тройки Хоара, выражающей свойство корректности некоторой

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

условий, начиная с крайних - предусловия и постусловия. При этом тройка

считается выведенной, если удастся вывести соответствующее точечное условие

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

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

относящемуся к другому концу некоторого фрагмента программы, полезно

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

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

конструктов.

Содержательно правила преодоления выражают своеобразные законы

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

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

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

предикатов.

Это особенно наглядно при преодолении фрагментов в естественном

порядке, слева направо. Однако и движение в противоположном направлении

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

доказательство ее корректности создаются одновременно.

Ведь постусловие выражает цель работы фрагмента программы. Поэтому

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

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

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

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

(постусловия) в исходный предикат (предусловие).

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

фрагмента программы слева направо (чтобы сосредоточить внимание на сущности

и приемах доказательства свойств программ).

15.2.6. Правила преодоления конструктов языка Д

Наша цель - научиться выводить постусловие из предусловия,

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

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

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

Замечание. Это означает, в частности, что верить нашему доказательству

нужно как раз "по модулю" доверия к правильности связи между дедуктивной и

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

что эта связь тщательно проверена. Впрочем, польза от доказательства не

столько в гарантии правильности (в общем случае, конечно, не обеспечиваемой;

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

точки зрения. Такое исследование, безусловно, способствует нахождению в

программе ошибок.

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

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

Состояние после выполнения конструкта в общем случае зависит от состояния

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

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

конструкта и, если нужно, с тройками, характеризующими вложенные конструкты.

Дедуктивная семантика присваивания. Начнем, например, преодолевать Ф(1-

2), т.е. по q(1) попытаемся построить разумное q(2). Каждый легко напишет

q(2) :: ( n >= 1 & x = M[1] )

Но это написано для конкретного предусловия и конкретного оператора

присваивания. Как же обобщить и формализовать прием преодоления

присваивания, примененный нами только что интуитивно? Ясно, что мы учли

результат выполнения конкретного оператора присваивания Ф(1-2) над

конкретными объектами программы x и M[1]. Другими словами, учли операционную

семантику присваивания. Результат выполнения состоит в том, что знак x

после выполнения оператора присваивания начинает обозначать то же самое, что

до его выполнения обозначал знак M[1]. Другими словами, денотат знака M[1]

становится денотатом знака x. Итак, если нам до выполнения присваивания что-

то известно про денотат знака M[1], то после выполнения присваивания то же

самое можно утверждать и про денотат знака x.

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

присваивания:

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

v := e

остается верным после выполнения этого оператора по отношению к значению

переменной v.

Осталось придумать, как формализовать эту идею в виде правила

преобразования логических формул.

Итак, наша задача - перейти от утверждения про e к утверждению про v,

причем первое справедливо до присваивания, второе - после. Присваивание

меняет значение v (и значение выражения e, если v в него входит). Поэтому в

общем случае предусловие само по себе не годится в качестве постусловия.

Нужно, во-первых, найти то, что сохраняется при присваивании (найти его

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

Ясно, что таким инвариантом служит всякое утверждение B про старое

значение выражения e. Если B истинно до присваивания, то останется истинным

и после - ведь старое значение выражения e не меняется. Но форма утверждения

B должна быть такой, чтобы и после преодоления присваивания B оставалось

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

просто в форме B(e), то оно может после присваивания стать ложным - у

выражения e может оказаться новое значение (каким образом?).

Поэтому обозначим (на метауровне, т.е. в наших рассуждениях о свойствах

программы) СТАРОЕ значение выражения e незанятой буквой, например Y, и

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

(Y = e) => B(Y)

т.е. (Y = e) влечет B(Y). При такой форме записи предусловия в нем явно

выделена инвариантная часть B(Y). Для аккуратности потребуем, чтобы

переменная v не входила в утверждение B. Теперь можно быть уверенными, что

B(Y) действительно не зависит от возможного изменения значения переменной v.

Теперь легко написать, что можно утверждать после присваивания. Ведь

старый денотат выражения e стал новым денотатом переменной v! Значит,

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

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

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