Доказательство правильности программ (стр. 2 )

1) если x, y, z принадлежат X, а х < у и у < z, то х < z;

2) для х и у из X справедлива одна и только одна из трех возможностей: либо х < у, либо у < х,  либо х = у;

3) если А – любое непустое подмножество X, то в А существует некоторый элемент х, такой, что х ≤ у для любого у, принадлежащего А.. Другими словами, любое непустое подмножество X содержит «наименьший элемент».

Отметим, что это определение касается обобщения структуры положительных (неотрицательных) целых чисел. Множество положительных целых чисел вполне упорядочено относительно обычного отношения <.

Пример 1.3. Множество всех целых не вполне упорядочено с помощью обычного отношения <. Такое множество обладает свойствами 1 и 2, но не обладает свойством 3. Множество всех отрицательных целых есть непустое подмножество множества целых, но не содержит наименьшего элемента.

Пример 1.4. Множество неотрицательных действительных чисел не является вполне упорядоченным с помощью обычного отношения <. Как и в предыдущем примере, для него выполняются свойства 1 и 2, но не выполняется свойство 3. Например, множество всех действительных чисел больше единицы, (такое множество можно обозначить следующим-образом: {х : х есть действительное и х > 1}) не содержит наименьшего элемента. Действительно, единица меньше любого элемента множества, но она множеству не принадлежит.

Пример 1.5. Множество всех упорядоченных пар неотрицательных целых чисел вполне упорядочено с помощью отношения лексикографического порядка <. Это отношение можно определить так: отношение (n1, n2) < (n3, n4) справедливо, если и только если (n1 < n3) или (n1 = n3  и  n1 < n4). В качестве упражнения покажите, что такое отношение обеспечивает нужную упорядоченность.

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

Принцип обобщенной индукции

Пусть X – вполне упорядоченное относительно < множество, а S(х) – некоторое высказывание, касающееся элемента х из X. Если требуется доказать справедливость S(х) для всех х, принадлежащих X, то необходимо:

1) доказать, что справедливо S(х0), где х0 – наименьший элемент в X;

2) доказать для всех х в X, удовлетворяющих условию х0 < х, что если справедливо S (у) для всех  у < х, то справедливо и S(х).

Отметим, что если X – множество положительных целых чисел, а отношение < имеет обычный смысл, то принцип обобщенной индукции идентичен принципу строгой индукции (разд. 1.1).

Чтобы убедиться в действенности принципа обобщенной индукции как метода доказательства, предположим, что S(х) – некоторое высказывание, для которого уже доказаны оба положения. Мы хотим сделать вывод о том, что S(х) справедливо для любых х в X. Предположим, что это не так. Пусть множество А = {х: х принадлежит X и S(х) ложно}. Если S(х) не справедливо для всех х в X, то А – непустое подмножество X. Так как X вполне упорядочено, то известно, что А содержит наименьший элемент а0. По определению это наименьший элемент X, для которого S(х) не справедливо, Таким образом, S(у) справедливо для всех у (если они есть), удовлетворяющих условию у < а0. Если а0 – наименьший элемент в X, то S(а0) справедливо, что следует из первого положения. В противном случае из справедливости S(у) для всех у < а0 и второго положения вытекает, что S(а0) справедливо. Но это противоречит предположению, что а0 принадлежит А и S(а0) ложно. Единственный способ устранить это противоречие – считать А пустым множеством, т. е. в X нет элементов, для которых высказывание S(х) ложно.

Пример 1.6. Рассмотрим последовательность чисел, определенную следу­ющим образом: S0, 0 = 0, а для любой другой пары неотрицательных чисел m, n

Например, первые элементы этой последовательности:

S0, 0 = 0, S1, 0 = S0, 0 + 1 = 0 + 1 = 1,

S0, 1 = S0, 0 + 1 = 1, S1, 1 = S1, 0 + 1 = 1 + 1 = 2,

S2, 0 = S1, 0 + 1 = 2, S2, 1 = S2, 0 + 1 = 3, ... .

Нужно доказать, что  Sm, n = m + n  для любых неотрицательных целых m, n. Используем принцип обобщенной индукции на множестве X упорядоченных пар неотрицательных целых чисел. Множество упорядочено на основе лексикографического порядка, описанного в примере 3. Чтобы доказать справедливость Sm, n = m + n для любых < m, n > в X, необходимо:

1) доказать, что Sm, n = m + n справедливо, если < m, n > – наименьший элемент в X. Но так как наименьший элемент – пара < 0, 0 >, то нужно показать, что S0, 0 = 0 + 0 = 0. Это очевидно по определению S0, 0;

2) доказать, что если Sm’, n’ = m’ + n’ справедливо для любых пар < m’, n’ > < < m, n >, то справедливо и Sm, n = m + n для любых < 0, 0 > < < m, n > в X. Предположим, что формула Sm’, n’ = m’ + n’ верна для < m’, n’ > < < m, n >. Это гипотеза индукции. Нужно показать, что Sm, n = m + n. Существует две возможности: либо
n = 0, либо n ≠ 0. Если n = 0, то по определению Sm, n = Sm–1, n + 1. Однако < m–1, n > < < m, n >, и, следовательно, по нашей гипотезе Sm–1, n = (m – 1) + n. Поэтому Sm, n = Sm–1, n+ 1 = = (m – 1 + n) + 1 =
= m + n. Если n ≠ 0, то Sm, n = Sm, n–1 + 1 по определению. Но
< m, n–1 > < < m, n > и по гипотезе Sm, n–1 = m + (n – 1). Следовательно, в этом случае Sm, n = Sm, n–1 + 1 = (m + n – 1) + 1 = m + n, что и требовалось доказать.

Глава 2. ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА правильности С ПОМОЩЬЮ ИДУКТИВНЫХ УТВЕРЖДЕНИЙ

В первой части конспекта лекций мы сформулировали и показали на примерах, как используется метод индуктивных утверждений. И формулировки индуктивных утверждений, и процесс доказательства проводились довольно неформальным образом. Если использовать какую-либо формальную нотацию для записи индуктивных утверждений и соответствующую дедуктивную систему для проведения доказательств, то можно формализовать весь этот процесс. В данной главе мы обсудим некоторые аспекты такой формализации. Если мы надеемся, что в конце концов придем к тому, что при поддержке некоторой «механической» системы будем либо выполнять доказательство, либо его проверять, то некоторого типа формализация нам необходима. Студенты, которых интересует вопрос формализации, могут обратиться к литературе [3, 4, 5]. Наиболее изученной формальной нотацией для формулирования и проведения математического доказательства является исчисление предикатов. Мы полагаем, что студент знаком с такого рода нотацией, либо предлагаем ему воспользоваться книгами по математической логике [7, 8] и самостоятельно ознакомиться с данными вопросами.

Напомним, что метод индуктивных утверждений состоит в следующем [1]. Для доказательства частичной правильности некоторой блок-схемы относительно утверждений А и С мы связываем утверждение А с начальной точкой блок-схемы, а утверждение С – с конечной. Кроме этого, необходимо выделить и связать с блок-схемой некоторые другие утверждения (описывающие отношения между значениями переменных, справедливые в момент попадания в соответствующую точку программы). Нужно, в частности, связать по крайней мере с одной из точек в замкнутом пути (цикле) одно такое утверждение. Затем необходимо для каждого пути в блок-схеме, ведущего из точки i с утверждением Аi в точку j с утверждение Аj при условии, что на пути из i в j нет промежуточных точек с утверждениями, доказать, что если мы находимся в точке i и справедливо утверждение Аi а затем переходим по нашему пути в точку j, то при попадании в эту точку будет справедливо утверждение Аj. Для формализации такого доказательства необходимо:

1) использовать некоторую формальную нотацию для записи утверждений;

2) формализовать то, что необходимо доказывать для каждого пути в блок-схеме;

3) использовать для выполнения доказательства некоторую формальную систему вывода (дедуктивную систему).

Развитие формальных методов вывода для выполнения доказательств не входит в круг вопросов, рассматриваемых в данном учебном пособии. Заинтересованный студент может познакомиться с этими вопросами в любом хорошем учебнике логики и учебном пособии [3]. Мы рассмотрим лишь вопросы, относящиеся к п. 1 и 2. Для цели, указанной в п. 1, можно использовать нотацию исчисления предикатов (или другую формальную нотацию). С ее помощью можно формулировать нужные утверждения. Исчисление предикатов не совсем подходит для формулирования индуктивных утверждений. Многие из них трудно (если вообще возможно) выразить с помощью этой нотации. Поиски наиболее подходящей формальной системы для записи индуктивных утверждений и проведения доказательств являются предметом современных исследований. Тем не менее здесь для выражения утверждений будет использоваться исчисление предикатов. Что касается п. 3, то надо дать некоторый систематический метод формирования для каждого из путей блок-схемы подлежащего доказательству формализованного высказывания. Множество всех таких высказываний, которые нужно доказывать для определения частичной правильности программы, иногда называют множеством условий верификации (verification conditions) для этой программы.

Для систематического формирования условий верификации некоторой блок-схемы поступим следующим образом. Рассмотрим по порядку все пути в блок-схеме. Предположим, что речь идет о пути из точки i в точку j. Утверждение, относящееся к точке i, обозначим через Аi (Х, Y, ...), где X,  Y, ...  – переменные, входящие в это утверждение. Аналогично обозначим и утверждение для точки j: Аj (Х, Y, ...). По пути из точки i в точку j значения переменных могут измениться (например, оператором присваивания). Для переменной V через epath (V) (изменение переменной вдоль пути) будем обозначать выражение, определяющее значение переменной V в точке j «в терминах» значений переменных в точке i и значений, присваиваемых переменным по мере прохождения пути. Если, например, на пути из i в j выполняется лишь пересылка X ← Y + 1, то epath (Х) = Y + 1, а epath (Y) = Y. Если на этом пути было три оператора присваивания  Х ← X + 1,
Y ← Y + Y и X ← Х + Y – 2, то epath (Х) = (Х + 1) + (Y + Y) – 2 =
= X + 2•Y – 1 и epath (Y) = Y + Y = 2•Y. Однако на пути из точки i в точку j может встретиться несколько точек, где выполняются проверки. Будем обозначать такие проверки через tk (Х, Y, ...), где k – указывает точку, к которой относится проверка, а X, Y, ... – переменные, от которых она зависит. Предположим, что tk (Х, Y, ...), ..., t1 (Х, Y, ...) – полный набор всех проверок, встречающихся в различных точках на пути из точки i в точку j. Для каждой из этих проверок (tm (Х, Y, ...)) сформулируем высказывание: