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

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

Оператор присваивания имеет вид: x := E, где x - простая переменная, E – выражение (типы x и E совпадают).

Определим слабейшее предусловие оператора присваивания как Q = wp(x := E, R), где Q получается из R заменой каждого вхождения x на E, что обозначим Q = R^x_Е.

Предполагается, что значение Е определено и вычисление выражения Е не может изменить значения ни одной переменной. Последнее ограничение запрещает функции с побочным эффектом. Следовательно, можно использовать обычные свойства выражений такие, как ассоциативность, коммутативность и логические законы.

Составной оператор имеет вид: begin S₁; S₂; ... ; S_n end

Определим слабейшее предусловие для последовательности двух операторов:

wp(S₁;S₂, R) = wp(S₁, wp(S₂, R)).

Аналогично слабейшее предусловие определяется для последовательности из n операторов.

Оператор выбора определим так:if B₁ → S₁ П B₂ → S₂ ... П B_n → S_n fi

Здесь n ³ 0, B₁, B₂, ..., B_n - логические выражения, называемые охранами, S₁, S₂, ..., S_n - операторы, пара B_i → S_i называется охраняемой командой, П - разделитель, if и fi играют роль операторных скобок.

Выполняется оператор следующим образом.

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

Выбирается одна из охраняемых команд B_i → S_i, у которой значение B_i истина, и выполняется S_i.

Определим слабейшее предусловие:

wp(if, R) = BB AND (B₁ => wp(S₁, R)) AND ... AND(B_n => wp(S_n, R)),

где BB = B₁ OR B₂ OR ... OR B_n.

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

Естественно определить wp(if, R) с помощью кванторов:

wp(if, R) = ($ i: 1 i n : B_i) AND("i: 1 i n : B_i => wp(S_i, R)).

Пример 2.4. Определить z = |x|.

С использованием оператора выбора :if x ³ 0 → z := x П x 0 → z := -x fi.

К особенностям оператора выбора следует отнести, во-первых, тот факт, что он включает условный оператор (if... then..), альтернативный оператор (if… then... else...) и оператор выбора (case).

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

В-третьих, благодаря отсутствию умолчаний, запись оператора выбора представлена в симметричном виде.

Оператор цикла. В обозначениях Э. Дейкстры цикл имеет вид: do B → S od.

Обозначим это соотношение через DO и представим его в следующем виде:

DO: do B₁ → S₁ П B₂ → S₂ ... П B_n → S_nod,

где n ³ 0, B_i → S_i - охраняемые команды.

Выполняется оператор следующим образом. Пока возможно выбирается охрана B_i со значением истина, и выполняется соответствующий оператор S_i. Как только все охраны будут иметь значение ложь, выполнение DO завершится.

Выбор охраны со значением истина и выполнение соответствующего оператора называется выполнением шага цикла. Если истинными являются несколько охран, то выбирается любая из них.

Следовательно, оператор DO эквивалентен оператору

do BB → ifB₂ → S₁ П B₂ → S₂ ... П B_n → S_nfi od или do BB → IF od,

где BB - дизъюнкция охран, IF- оператор выбора.

Пример 2.5. Алгоритм Евклида.

Вариант 1.

задать (N, M);

if N > 0 AND M > 0 → n, m := N, M;

do n ≠ m → if n > m → n := n – m П m > n → m := m – n fi od;

выдать (n)

fi.

Вариант 2.

задать (N, M);

if N > 0 AND M > 0 → n, m := N, M;

do n > m → n := n – m П m > n → m := m – n od;

выдать (n)

fi.

Дадим формальное определение слабейшего предусловия для оператора цикла DO.

Пусть предикат H₀(R) определяет множество состояний, в которых выполнение DO завершается за 0 шагов (в этом случае все охраны с самого начала ложны, после завершения R имеет значение истина):

H₀(R) = NOT BB AND R.

Другими словами, требуется, чтобы оператор цикла DO завершил работу, не производя выборки охраняемой команды, что гарантируется первым конъюнктивным членом предиката H₀(R): NOT BB = T. При этом истинность R до выполнения DO является необходимым условием для истинности R после выполнения DO.

Определим предикат H_k(R) как множество состояний, в которых выполнение DOзаканчивается за k шагов при значении R истина (H_k(R) будет определяться через H_k-1(R)):

H_k(R) = H₀(R) OR wp(IF, H_k-1(R)), k > 0 → wp(DO, R) = ($ k: k ³ 0: H_k(R)).

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

Определение DO. Если предикаты H_k(R) задаются в виде

H_k(R) = NOT B ANDR, k = 0,

H_k(R) = wp(IF, H_k-1(R)), k > 0, → wp(DO, R)=($ k: k ³ 0: H_k(R)).

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

(P ANDBB) => wp(IF, R).(2.3)

Тогда для оператора цикла справедливо:

(P AND wp(DO, T)) => wp(DO, P AND NOT BB).

Эта теорема известна как основная теорема инвариантности для цикла. Предикат Р, истинный перед выполнением и после выполнения каждого шага цикла, называется инвариантным отношением или просто инвариантом цикла. В математике термин «инвариантный» означает не изменяющийся под воздействием совокупности рассматриваемых математических операций.

Поясним смысл теоремы. Условие (2.3) означает, что если предикат P первоначально истинен и одна из охраняемых команд выбирается для выполнения, то после ее выполнения P сохранит значение истинности. После завершения оператора, когда ни одна из охран не является истиной, будем иметь:

P AND NOTBB.

Работа завершится правильно, если условие wp(DO, T) справедливо и до выполнения DO. Так как любое состояние удовлетворяет T, то wp(DO, T) является слабейшим предусловием для начального состояния такого, что запуск оператора цикла DO приведет к правильно завершаемой работе.

Доказательство.

Из определения DO следует:

H₀(T) = NOT BB ANDT, k = 0;

H_k(T) = wp(IF, H_k-1(T)), k > 0, → wp(DO, T) = ($ k: k ³ 0: H_k(T));

H₀(P AND NOT BB) = P AND NOT BB;

H_k(P AND NOT BB) = wp(IF, H_k-1(P AND NOT BB), → wp(DO, P AND NOT BB) = = ($ k ³ 0: H_k(P AND NOT BB)).

С помощью метода математической индукции можно доказать, что из условия (2.3) следует

(P AND H_k(T)) => H_k(P AND NOT BB), k ³ 0.

Тогда имеем

P AND wp(DO, T) = ($ k: k ³ 0: P AND H_k(T)) => ($ k: k ³ 0: H_k(P AND NOT BB)) = = wp(DO, P AND NOT BB).

Следовательно, (P AND wp(DO, T)) => wp(DO, P AND NOT BB).

Чтобы использовать аксиоматическую семантику с данным языком программирования для доказательства правильности программ или для описания формальной семантики, для каждого вида операторов языка должны быть определены аксиомы или правила логического вывода. С ними мы познакомимся в п. 2.3 «Верификация программ».

В аксиоматической семантике система (2.1) интерпретируется как набор аксиом в рамках некоторой формальной логической системы, в которой есть правила вывода и/или интерпретации определяемых объектов.

Для интерпретации системы функций (2.1) вводится понятие аксиоматического описания <S, A> - логически связанной пары понятий: S - сигнатура используемых в системе символов функций f₁, f₂, ..., f_m и символов констант (нульместных функциональных символов) c₁, c₂, ..., c_l, а A - набор аксиом, представленный системой. Предполагается, что каждая переменная x_i, i = 1, ..., k, и каждая константа c_i, i = 1, ..., l, используемая в A, принадлежит к какому-либо из типов данных t₁, t₂, ..., t_r, а каждый символ f_j, j = 1, ..., m, представляет функцию, типа: t_i1 t*_i2t*... _ik t_i0. Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных t_i = t_i', i = 1, ..., r, и конкретные значения констант c_i = c_i', i = 1, ..., l.

К. Хоaр построил аксиоматическое определение набора типов данных, которые потом Н. Вирт использовал при создании языка Паскаль.

Пример 2.6. Рассмотрим систему равенств:

УДАЛИТЬ(ДОБАВИТЬ(m,d)) = m,

ВЕРХ(ДОБАВИТЬ(m,d)) = d,

УДАЛИТЬ(ПУСТ) = ПУСТ,

ВЕРХ(ПУСТ) = ДНО,

где УДАЛИТЬ, ДОБАВИТЬ, ВЕРХ - символы функций, а ПУСТ и ДНО - символы констант, образующие сигнатуру этой системы. Пусть D, D1 и М - некоторые типы данных, такие, что m M, d D, ПУСТ M, ДНО D1, а функциональные символы представляют функции следующих типов:

УДАЛИТЬ: M M,

ДОБАВИТЬ:M, D M,

ВЕРХ:M D1.

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

Зададим интерпретацию символов ее сигнатуры: D - множество значений, которые являются элементами магазина, M - множество состояний магазина, M = {d₁,d₂, ... ,d_n: d_i D, i = 1, ..., n, n ³ 0}, D1=D {ДНО}, ПУСТ={}, а ДНО - особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяют свойства магазина.

При определении семантики полного языка программирования с использованием аксиоматического метода для каждого вида операторов языка должны быть сформулированы аксиома или правило логического вывода. Но определение аксиом и правил логического вывода для некоторых операторов языков программирования - очень сложная задача. Трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства высказываний о программах» (Э. Дейкстра).

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

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

Денотационная семантика

Денотационная семантика - самый строгий широко известный метод описания значения программ. Она прочно опирается на теорию рекурсивных функций. Всестороннее рассмотрение денотационной семантики - длительное и сложное дело. Здесь мы познакомимся лишь с ее основными принципами.

Основной концепцией денотационной семантики является определение для каждой сущности языка некоего математического объекта и некоей функции, отображающей экземпляры этой сущности в экземпляры этого математического объекта. Поскольку объекты определены строго, то они представляют собой точный смысл соответствующих сущностей. Сама идея основана на факте существования строгих методов оперирования математическими объектами, а не конструкциями языков программирования. Сложность использования этого метода заключается в создании объектов и функций отображения. Название метода «денотационная семантика» происходит от английского слова denote (обозначать), поскольку математический объект обозначает смысл соответствующей синтаксической сущности.

Для введения в денотационный метод мы используем очень простую языковую конструкцию - двоичные числа. Синтаксис этих чисел можно описать следующими грамматическими правилами:

<двоичное_число> → 0; | 1; | <двоичное_число>0; | <двоичное_число>1.

Для описания двоичных чисел с использованием денотационной семантики и грамматических правил, указанных выше, их фактическое значение связывается с каждым правилом, имеющим в своей правой части один терминальный (основной) символ. Объектами в данном случае являются десятичные числа.

В нашем примере значащие объекты должны связываться с первыми двумя правилами. Остальные два правила являются, в известном смысле, правилами вычислений, поскольку они объединяют терминальный символ, с которым может ассоциироваться объект, с нетерминальным, который может представлять собой некоторую конструкцию.

Пусть область определения семантических значений объектов представляет собой множество неотрицательных десятичных целых чисел Nat. Это именно те объекты, которые мы хотим связать с двоичными числами. Семантическая функция М_b отображает синтаксические объекты в объекты множества N согласно указанным выше правилам. Сама функция М_b определяется следующим образом:

М_b('0') = 0, М_b('1')=1;

М_b(<двоичное_число> '0') = 2 × М_b(<двоичное_число>);

М_b(<двоичное_число> ‘1’) = + 2 × М_b(<двоичное_число>) + 1.

Мы заключили синтаксические цифры в апострофы, чтобы отличать их от математических цифр. Отношение между этими категориями подобно отношениям между цифрами в кодировке ASCII и математическими цифрами. Когда программа считывает число как строку, то прежде, чем это число сможет использоваться в программе, оно должно быть преобразовано в математическое число.

Пример 2.7. Описание значения десятичных синтаксических литеральных констант.

<десятичное_число> → 0|1|2|3|4|5|6|7|8|9;

| <десятичное_число> (0|1|2|3|4|5|6|7|8|9).

Денотационные отображения для этих синтаксических правил имеют следующий вид:

M_d(‘0') = 0, M_d('1') = 1, ,..., M_d('9') = 9;

М_d(<десятичное_число> '0') = 10 × М_d(<двоичное_число>);

М_d(<десятичное_число> ‘1’) = 10 × М_d(<десятичное_число>) + 1;

…

М_d(<десятичное_число> '9') = 10 × М_d(<десятичное_число>) + 9.

Денотационную семантику программы можно определить в терминах изменений состояний идеального компьютера. Подобным образом определялись операционные ceмантики, приблизительно так же определяются и денотационные. Правда, для простоты они определяются только в терминах значений всех переменных, объявленных в программе. Операционная и денотационная семантики различаются тем, что изменения состояний в операционной семантике определяются запрограммированными алгоритмами, а в денотационной семантике они определяются строгими математическими функциями. Пусть состояние s программы определяется следующим набором упорядоченных пар: {<i₁, v₁>, <i₂, v₂>, …, <i_n, v_n>}.

Каждый параметр i является именем переменной, а соответствующие параметры v являются текущими значениями данных переменных. Любой из параметров v может иметь специальное значение undef, указывающее, что связанная с ним величина в данный момент не определена.

Пусть VARMAP - функция двух параметров, имени переменной и состояния программы. Значение функции VARMAP(i_k, s) равно v_k (значение, соответствующее параметру i_k в состоянии s).

Большинство семантических функций отображения для программ и программных конструкций отображают состояния в состояния. Эти изменения состояний используются для определения смысла программ и программных конструкций. Отметим, что такие языковые конструкции, как выражения, отображаются не в состояния, а в величины.

Выражения являются основой большинства языков программирования. Более того, мы имеем дело только с очень простыми выражениями. Единственными операторами являются операторы + и ×; выражения могут содержать не более одного оператора; единственными операндами являются скалярные переменные и целочисленные литеральные константы; круглые скобки не используются; значение выражения является целым числом. Ниже следует описание этих выражений в форме БНФ:

<выражение> → <десятичное_число>| <переменная>

| <двоичное_выражение>

<двоичное_выражение> → <выражение_слева><оператор>

<выражение_справа>

<оператор> → + | ×

Единственной рассматриваемой нами ошибкой в выражениях является неопределенное значение переменной. Разумеется, могут появляться и другие ошибки, но большинство из них зависят от машины. Пусть Z - набор целых чисел, a error - ошибочное значение. Тогда множество Z {error} является множеством значений, для которых выражение может быть вычислено.

Ниже приведена функция отображения для данного выражения Е и состояния s. Символ º обозначает равенство по определению функции.

M_e(<выражение>, s) º

case<выражение> of

<десятичное_число> => M_d(<десятичное_число>, s)

<переменная> =>if VARMAP(<переменная>, s) = undef

then error

else VARMAP(<переменная>, s)

<двоичное_выражение> =>

if(M_e(<двоичное_выражение>.<выражение_слева>, s) = undef

OR M_e(<двоичное_выражение>.< выражение_справа >, s) = undef)

then error

else if (<двоичное_выражение>.< оператор > = '+' then

M_e(<двоичное_выражение>.<выражение_слева>, s) +

M_e(<двоичное_выражение>.<выражение_справа>, s)

else M_e(<двоичное_выражение>.<выражение_слева>, s) ×

M_e(<двоичное_выражение>.<выражение_справа>, s).

Оператор присваивания - это вычисление выражения плюс присваивание его значения переменной, находящейся в левой части. Сказанное можно описать следующей функцией:

М_а(х = Е, s) º if M_e(E, s) = error

then error

else s' = {<i₁', v₁'>, <i₂', v₂'>,..., <i_n', v_n'>} where

for j = 1, 2, ..., n, v_j' = VARMAP(i_j', s) if i_j <>x;

M_e(E, s) ifi_j = x.

Отметим, что два сравнения, выполняющиеся в двух последних строках(i_j <> x и i_j = х), относятся к именам, а не значениям.

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

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

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

Декларативная семантика

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

Основная концепция декларативной семантики заключается в том, что существует простой способ определения смысла каждого оператора, и он не зависит от того, как именно этот оператор используется для решения задачи. Декларативная семантика значительно проще, чем семантика императивных (применяющихся в компьютерах с фон-неймановской архитектурой) языков. Она не требует для проверки отдельного оператора рассмотрения его контекста, локальных объявлений или последовательности выполнения программы.

Формальное определение семантики становится общепринятой частью определения нового языка. Стандартное описание языка PL/I включает в себя VDL-подобную нотацию, описывающую семантику операторов PL/I, а для языка Ada было разработано определение на основе денотационной семантики. Тем не менее, изучение формальных определений семантики не оказало такого сильного влияния на практическое определение языков, как изучение формальных грамматик — на определение синтаксиса. Ни один из методов определения семантики не оказался по настоящему полезным ни для пользователя, ни для разработчиков компиляторов языков программирования.

Не нашли, что искали? Воспользуйтесь поиском по сайту: