Книга: Основы объектно-ориентированного программирования

Дополнительные темы

Представленное выше описание абстрактных типов данных вполне достаточно для использования АТД в рамках данной книги. (Чтобы дополнить его, выполните упражнения, которые помогут уточнить ваше понимание этого понятия).

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

[x]. неявность и ее связь с процессом конструирования ПО;

[x]. различие между спецификацией и проектированием;

[x]. различие между классами и записями;

[x]. возможные альтернативы использованию частичных функций;

[x]. решение о полноте или неполноте спецификации.

Библиографические ссылки к этой лекции указывают на более специальную литературу по АТД.

Еще раз о неявности

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

Вполне законен вопрос о различии между упрощенной спецификацией АТД, использующей объявление функций

x: POINT REAL
y: POINT REAL

и объявлением типа в таком традиционном языке программирования, как Pascal:

type
POINT =
record
x, y: real
end

На первый взгляд эти два объявления представляются эквивалентными: оба утверждают, что с типом POINT связаны два значения x и y типа REAL. Но между ними имеется существенная, хотя и тонкая разница:

[x]. Запись в языке Pascal является законченной и явной: она показывает, что объект POINT включает два данных поля и ничего кроме них.

[x]. Объявление функций АТД не несут такого смысла. Они показывают, что объект типа POINT можно запрашивать о значениях его x и y, но не исключают других запросов, например, о массе и скорости точки в кинематическом приложении.

С упрощенной математической точки зрения можно считать, что приведенное выше объявление в Паскале является определением математического множества POINT как декартова произведения:

POINT REAL ? REAL,

где знак означает "определяется как" ("равно по определению"), и оно полностью задает POINT. В отличие от этого спецификация АТД не определяет явно POINT посредством такой математической модели как декартово произведение, она просто неявно характеризует POINT, перечисляя два запроса, применимых к объектам этого типа.

Если имеются спецификации некоторого понятия, то может появиться желание переместить ее из неявного мира в явный, идентифицируя понятие с декартовым произведением применимых к нему простых запросов, например захочется идентифицировать точки с парами <x, y>. Такой процесс идентификации можно рассматривать как определение перехода от анализа и спецификации к проектированию и реализации.

Соотношение спецификации и проектирования

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

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

Приведенное выше определение дает более точный критерий: пересечь Рубикон между спецификацией и проектированием - это перейти от неявного к явному, другими словами:

Определение: переход от анализа (спецификации) к проектированию

Перейти от спецификации к проектированию - это идентифицировать каждую абстракцию с декартовым произведением ее простых запросов.

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

Соотношение классов и записей

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

class POINT feature
x, y: REAL
end

Это выглядит подозрительно похожим на приведенное выше определение записи в Паскале. Но, несмотря на внешнее сходство, определение класса другое - оно неявное! Эта неявность проявляется при наследовании: автор класса или (что еще более интересно) кто-либо другой может в любой момент определить новый класс, например:

class MOVING_POINT inherit
POINT
feature
mass: REAL
velocity: VECTOR [REAL]
end

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

p1: POINT

может быть связана с объектом не только типа POINT, но и с каждым потомком этого типа, например с объектом типа MOVING_POINT. Это может получиться, в частности, с помощью "полиморфных присваиваний" вида:

p1 := mp1
где mp1 имеет тип MOVING_POINT.

Эти возможности иллюстрируют неявность и открытость определения класса: соответствующие экземпляры представляют не только точки в узком смысле, т. е. непосредственно экземпляры класса POINT, но и экземпляры всякого класса, описывающего понятия, выводимые из исходного класса.

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

Альтернативы частичным функциям

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

Конечно, это не единственно возможное решение. Другим способом, который приходит на ум и действительно используется в некоторых работах по АТД, является превращение частичной функции во всюду определенную за счет введения специального значения "ошибка" для случаев применения функции к неподходящим аргументам.

Каждый тип T дополняется значением "ошибка". Обозначим его через w_T . Тогда для всякой функции f сигнатура

f: ... Типы входов ... T

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

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

Предположим, например, что рассматриваются стеки целых чисел - экземпляры типа STACK [INTEGER], где INTEGER - это АТД, экземпляры которого - целые числа. Хотя для нашего примера не требуется полностью выписывать спецификацию INTEGER, этот АТД должен моделировать основные операции (сложение, вычитание, "меньше чем" и т. п.), определенные на математическом множестве целых чисел. Аксиомы этого АТД должны выражать обычные свойства целых чисел. Вот одно из таких типичных свойств: для всякого целого n:

[Z1]
n + 1 n

Пусть теперь n будет результатом запроса верхнего элемента пустого стека, т. е. значением выражения item (new), где new - это пустой стек целых чисел. При этом запросе n должно получить специальное значение w_INTEGER . Что же тогда должно быть значением выражения n+1? Если у нас в распоряжении имеются в качестве значений только обычные целые числа и w_INTEGER , то в качестве ответа мы вынуждены выбрать w_INTEGER:

wINTEGER + 1 = wINTEGER.

Это единственный допустимый выбор. Если присвоить w_INTEGER+1 любое другое значение, "нормальное" число q, то это означает, что после попытки доступа к вершине пустого стека и получения в качестве результата ошибочного значения мы можем волшебным образом устранить всякую память об этой ошибке, просто прибавив к результату единицу!

Но, при выборе w_INTEGER в качестве значения n + 1 при n равном w_INTEGER, нарушается указанное выше свойство Z1. В общем случае, выражение w_INTEGER+p будет равно w_INTEGER для любого p. Это означает, что для измененного типа данных (INTEGER, дополненные ошибочным элементом) требуется новая система аксиом, объясняющая, что всякая операция над целыми числами возвращает значение w_INTEGER, если хоть один из ее аргументов равен w_INTEGER. Аналогичные изменения потребуются для каждого типа.

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

Полна ли моя спецификация?

Другой вопрос, который может вас тревожить: есть ли какой-нибудь способ убедиться в том, что спецификация описывает все нужные свойства объектов, для которых она предназначена? Студенты, которым требуется написать их первые спецификации (например, проделать упражнения в конце этой лекции), часто приходят с аналогичным вопросом: "Как узнать, что я уже специфицировал достаточно свойств и могу остановиться?"

В более общей форме вопрос звучит так: существует ли метод, позволяющий определять полноту спецификации АТД?

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

[x]. Если эталонный документ является неформальным (например, документом с требованиями на естественном языке или просто текстом упражнения), то отсутствие формальности предотвращает всякую попытку систематической проверки соответствия спецификации всем требованиям, описанным в этом документе.

[x]. Если же эталонный документ является формальным, и мы можем, используя его, проверить полноту нашей спецификации, то это просто отодвигает проблему дальше: как можно убедиться в полноте самого эталонного документа?

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

Как можно перенести эту идею на спецификации АТД? Здесь "язык теории" - это множество правильно построенных выражений, т.е. тех выражений, которые можно построить, используя функции АТД, применяемые к аргументам соответствующих типов. Например, используя спецификацию АТД STACK и считая, что x является правильно построенным выражением типа G, можно указать следующие правильно построенные выражения:

new

put (new, x)

item (new) - если это кажется странным, то см. комментарии ниже.

empty (put (new, x))

stackexp - ранее определенное сложное выражение.

Однако выражения put (x) и put (x, new) не являются правильно построенными, так как они не соответствуют правилу: put всегда должно иметь два аргумента - первый типа STACK [G] и второй типа G.

Третий пример в рамке item (new) не задает никакого осмысленного вычисления, поскольку аргумент new не удовлетворяет предусловию для item. Хотя это выражение и правильно построено, оно не является корректным. Вот точное определение этого понятия.

Определение: корректное выражение АТД

Пусть f(x1 , ... , xn) - правильно построенное выражение, содержащее одну или более функций некоторого АТД. Это выражение является корректным тогда и только тогда, когда все его аргументы xi являются (по рекурсии) корректными и их значения удовлетворяют предусловию f, если оно имеется.

Не следует путать "корректное" и "правильно построенное". "Правильно построенное" - это структурное свойство, указывающее на то, что функции, входящие в выражение, имеют правильное число аргументов соответствующих типов, а корректность, которой могут обладать лишь правильно построенные выражения, означает, что данное выражение задает осмысленное вычисление. Как мы видели, выражение put (x) не является правильно построенным (и поэтому бессмысленно спрашивать, корректно ли оно), а выражение item (new) правильно построено, но некорректно.

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

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

empty (put (put (new, x1), x2))
item (put (put (new, x1), x2))
stackexp

Выражение-запрос задает значение, которое (если оно определено) принадлежит не определяемому АТД, а некоторому другому ранее определенному типу. Так, первое приведенное выше выражение имеет значение типа BOOLEAN, а второе и третье - тип G формального параметра для элементов стека, например если мы рассматриваем АТД STACK [INTEGER], то это будет тип INTEGER.

Выражения-запросы представляют внешние наблюдения, которые можно сделать о результатах некоторого вычисления, использующего экземпляры нового АТД. Если спецификация этого АТД хорошая, то она должна позволить нам установить определены ли эти результаты, и если да, то каковы они. Представляется, что спецификация стека обладает этим свойством, по крайней мере, для трех представленных в примере выражений, поскольку она позволяет установить, что все эти выражения определены, и с помощью аксиом можно получить их значения:

empty (put (put (new, x1), x2)) = False
item (put (put (new, x1), x2)) = x2
stackexp = x4

Эти наблюдения, перенесенные на произвольные спецификации АТД, приводят к прагматическому понятию полноты, известному как достаточная полнота, она означает, что спецификация содержит достаточно сильные аксиомы, которые позволяют находить для любого выражения-запроса его результат в виде некоторого простого значения.

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

Определение: достаточная полнота

Спецификация АТД T является достаточно полной тогда и только тогда, когда аксиомы ее теории позволяют для каждого выражения expr решить следующие задачи:

[x]. (S1) Определить, является ли expr корректным.

[x]. (S2) Если expr - выражение-запрос и в пункте S1 установлена его корректность, то представить значение expr в виде, не включающем никаких значений типа T.

В S2 выражение expr имеет вид f(x1 , ..., xn), где f - функция вида запрос такая, как empty и item для стеков. S1 говорит о том, что у expr есть значение, но этого недостаточно, нам хотелось бы знать, каково это значение, представленное в терминах значений других типов (в примере со стеком это значения типов BOOLEAN и G). Если аксиомы настолько сильны, что всегда позволяют ответить на этот вопрос, то спецификация является достаточно полной.

Достаточная полнота свидетельствует о том, что никакое важное свойство не осталось вне нашей спецификации. Поэтому ее можно считать ответом на поставленный выше вопрос: как понять, что можно прекратить поиски новых свойств при построении спецификации? На практике хорошо бы проводить такую проверку, по крайней мере неформально, для любой спецификации АТД, которую вы пишете - начните с решений упражнений, приведенных в этой лекции. Часто, можно получить формальное доказательство достаточной полноты; приведенное ниже доказательство для спецификации STACK является образцом, которому во многих случаях можно следовать.

Пункт S2 оптимистически говорит об одном значении expr, а что, если аксиомы приводят к двум или более значениям? Это сделало бы спецификацию бесполезной. Чтобы устранить такую ситуацию нам нужно еще одно свойство, называемое в математической логике непротиворечивостью:

Определение: непротиворечивость АТД

Спецификация АТД является непротиворечивой тогда и только тогда, когда для всякого правильно построенного выражения expr ее аксиомы позволяют вывести не более одного значения.

Эти два свойства являются взаимно дополнительными. Нам хотелось бы для каждого выражения-запроса выводить ровно одно значение: хотя бы одно (достаточная полнота), но не более одного (непротиворечивость).

Доказательство достаточной полноты

(Этот раздел и остаток этой лекции содержат дополнительный материал и их результаты не нужны для остальной части книги).

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

Несмотря на это, часто удается доказать достаточную полноту и непротиворечивость конкретной спецификации АТД. Чтобы удовлетворить любопытство читателей-любителей математики, в заключение этой лекции мы приведем доказательство того, что спецификация STACK на самом деле является достаточно полной. Доказательство ее непротиворечивости будет оставлено в качестве упражнения.

Для доказательства достаточной полноты спецификации стека нужно придумать эффективное правило для решения указанных выше задач S1 и S2, другими словами, такое правило, которое позволит нам для любого стекового выражения e:

[x]. (S1) Определить, является ли e корректным.

[x]. (S2) Если в пункте S1 установлена корректность e и его внешними функциями являются item или empty (т.е. функции-запросы), то представить значение e с помощью значений типов BOOLEAN и G без ссылок на значения типа STACK [G] или на функции из спецификации STACK.

Для начала мы рассмотрим только правильно построенные выражения, не включающие ни одну из двух функций-запросов item и empty, т. е. выражения, построенные только из функций new, put и remove. Таким образом, на этом этапе нас будет интересовать лишь задача S1 (установить определено ли выражение). Функции-запросы и S2 будут рассмотрены далее.

Правило для решения задачи S1 задается следующим свойством:

Правило корректного веса

Правильно построенное стековое выражение e, не содержащее ни item, ни empty, является корректным тогда и только тогда, когда его вес неотрицателен и каждое его подвыражение является (по индукции) корректным.

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

Определение: вес

Вес правильно построенного стекового выражения, не содержащего ни item, ни empty, определяется по индукции следующим образом:

[x]. (W1) Вес выражения new равен 0.

[x]. (W2) Вес выражения put (s, x) равен ws + 1, где ws - это вес s.

[x]. (W3) Вес выражения remove (s) равен ws- 1, где ws - это вес s.

Содержательно, правило корректного веса утверждает, что стековое выражение корректно тогда и только тогда, когда в нем самом и в каждом из его подвыражений имеется не меньше операций put (вставляющих элементы в стек), чем операций remove (выталкивающих элементы с вершины стека). Если рассмотреть такое выражение как представление некоторого вычисления над стеком, то это означает, что мы никогда не будем пытаться вытолкнуть больше элементов, чем втолкнули. Напомним, что на этом этапе мы сосредоточились на функциях put и remove, оставив в стороне запросы item и empty.

Интуитивно сформулированное правило выглядит верным, но нам следует все же доказать, что оно имеет место. Удобно ввести еще одно вспомогательное правило и одновременно доказывать справедливость обоих этих правил:

Правило нулевого веса

Пусть e - это правильно построенное и корректное стековое выражение, не содержащее item или empty. Тогда empty (e) истинно тогда и только тогда, когда вес e равен 0.

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

Аксиомы стека

Для всех x: G, s: STACK [G]

[x]. (A3) empty (new)

[x]. (A4) not empty (put (s, x))

При уровне вложенности 0 (без скобок) выражение e должно совпадать с new, поэтому его вес равен 0 и оно корректно, так как у new нет никаких предусловий. Аксиома A3 утверждает, что empty (new) истинно. Это обеспечивает базис индукции как для правила корректного веса, так и для правила нулевого веса.

Индукционный шаг: предположим, что оба правила выполняются для всех выражений с уровнем вложенности не более n. Нужно доказать, что тогда они выполняются и для любого выражения e с уровнем вложенности n+1. Поскольку наши выражения сейчас не содержат функций-запросов, то e должно иметь один из следующих двух видов:

E1 · e = put (s, x)
E2 · e = remove (s)

где x имеет тип G, а уровень вложенности у s равен n. Пусть ws - это вес s.

В случае E1, поскольку put - всюду определенная функция, e корректно тогда и только тогда, когда s корректно, т. е. (по предположению индукции) тогда и только тогда, когда s и все его подвыражения имеют неотрицательные веса. Но это эквивалентно тому, что e и все его подвыражения имеют неотрицательные веса, что и доказывает правило корректного веса в этом случае. Кроме того, e имеет положительный вес ws+1, и (по аксиоме A4) является непустым, что доказывает правило нулевого веса.

В случае E2 выражение e корректно тогда и только тогда, когда выполняются два следующих условия:

EB1 _ s и все его подвыражения являются корректными.
EB2 _ not empty (s) (это предусловие для функции remove).

По предположению индукции условие EB2 означает, что вес s ws положителен или, что эквивалентно, вес e, равный ws - 1, является неотрицательным. Следовательно, e удовлетворяет Правилу корректного веса. Чтобы доказать, что оно также удовлетворяет правилу нулевого веса, нужно показать, что e пусто тогда и только тогда, когда его вес равен 0. Так как вес s положителен, то s должно содержать по крайней мере одно вхождение put, которое также входит и в e. Рассмотрим самое внешнее вхождение put в e, это вхождение находится непосредственно внутри remove (так как remove находится на самом внешнем уровне у e). Это означает, что у e имеется подвыражение (быть может, совпадающее с самим e) вида

remove (put (stack_expression, g_expression)),

которое по аксиоме A2 можно сократить просто до stack_expression. После выполнения этой замены вес e уменьшится на 2, и получившееся выражение, имеющее то же значение, что и e, удовлетворяет по предположению индукции правилу нулевого веса. Это доказывает утверждение индукции в случае E2.

Это доказательство попутно показывает, что во всяком правильно построенном выражении, не содержащем функций-запросов item и empty, можно устранить все вхождения remove, т.е. получить, применяя всюду, где это возможно, аксиому A2, некоторую каноническую форму, в которую будут входить только put и new. Например, выражение:

put (remove (remove (put (put (remove (put (put (new, x1), x2)), x3), x4))), x5)

имеет то же значение, что и каноническая форма:

put (put (new, x1), x5).

Давайте дадим этому механизму имя и приведем его определение:

Правило канонического сокращения

Всякое правильно построенное и корректное стековое выражение, не содержащее функций-запросов item и empty, имеет эквивалентную каноническую форму, которая не содержит функции remove (т.е. состоит только из функций put и new>). Эта каноническая форма получается путем применения аксиомы стека A2 всегда, пока это возможно.

Таким образом, мы завершили доказательство достаточной полноты, но только для выражений, не содержащих функции-запросы, и, следовательно, только свойства S1 (проверка корректности выражения). Для завершения доказательства нужно рассмотреть выражения, включающие функции-запросы, и обсудить задачу S2 (нахождение значений для выражений-запросов). Это означает, что нам нужно некоторое правило для определения корректности и значения всякого правильно построенного выражения вида f(s), где s - это правильно построенное выражение, а f - это либо item, либо empty.

Это правило и доказательство его корректности также используют индукцию по уровню вложенности. Пусть n - это уровень вложенности s. Если n=0, то s может быть только new, поскольку остальные функции требуют аргументов и, следовательно, содержат хоть одну пару скобок. Тогда для обеих функций-запросов ситуация ясна:

[x]. empty (new) корректно и имеет значение истина (true) (по аксиоме A3);

[x]. item (new) некорректно, так как предусловие item требует выполнения not empty (s) .

Индукционный шаг: предположим, что s имеет уровень вложенности n не менее 1. Если у какого-либо подвыражения u выражения s внешняя функция есть item или empty, то уровень вложенности u не превосходит n-1, что по предположению индукции позволяет определить корректность u и, если u корректно, получить его значение, применяя аксиомы. Выполнив замены всех таких подвыражений, получим для s эквивалентную форму, в которую входят только функции put, remove и new.

Далее используем идею введенной выше канонической формы, чтобы избавиться от всех вхождений remove, так что результирующая форма для s будет включать только функции put и new. Случай, когда s это просто new уже был рассмотрен, остался случай, когда s имеет вид put(s', x) . В этом случае для двух рассматриваемых выражений имеем:

[x]. empty (s) корректно и по аксиоме A3 значение этого выражения есть ложь (false);

[x]. item (s) корректно, так как предусловие not empty (s) для item выполнено; из аксиомы A1 следует, что значение этого выражения равно x.

Это завершает доказательство достаточной полноты, так как мы показали справедливость множества правил - правила корректного веса и правила канонического сокращения, позволяющего нам выяснять корректность заданного стекового выражения, а для корректного выражения-запроса - определять его значение в терминах значений типов BOOLEAN и G.

Оглавление книги