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

Доказательное программирование — это составление программ с доказательством их правильности. Сложность составления и доказательства правильности алгоритмов и программ состоит в следующем.

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

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

Существуют два подхода к проверке программ — прагматический и доказательный. При прагматическом подходе проверка программ выполняется на ЭВМ путем тестирования.

Тестирование — это проверка программ на ЭВМ с помощью некоторого набора тестов. Ясно, что тестирование не дает гарантий правильности выполнения программ на всех допустимых данных. Следовательно, тестирование в общем случае не может дать и не дает полных гарантий отсутствия ошибок в программах.

Напомним, что отладка программ — это процесс поиска и исправления ошибок в программах на ЭВМ. Однако поскольку поиск ошибок при отладке программ проводится с помощью тестов, то полных гарантий нахождения и исправления всех ошибок в программах отладка не дает и в принципе дать не может.

По этой же причине неясно, когда процесс отладки программ — процесс поиска и исправления ошибок на ЭВМ — может считаться завершенным. А выявлены или нет все ошибки в программе при ее отладке не может сказать никто.

Таким образом, прагматический подход чреват созданием программ, содержащих ошибки даже после «завершения» отладки, что и наблюдается практически во всех больших программах для ЭВМ.

Рассмотрим в качестве иллюстрации принципов тестирования алгоритм и программу вычисления максимума из трех чисел: а, b, с.

алг «максимум трех чисел» 'максимум трех чисел

нач cls

ввод (а, b, с) input a, b, с

если а > b то if а > b then

тах:= a max = a

инеc b > с то elseif b > с then

тах:= b mах = b

инеc с > а то elseif с > a then

тах:= с mах = с

кесли end if

вывод («тах=»,тах)? «mах=»; mах

кон end

Запуск этой программы на ЭВМ можно проверить на следующих данных:

Tecт₁ Тест₂ Тест₃

? 1 1 2? 1 2 3? 3 2 1

max = 2 max = 3 max = 3

 

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

 

Контрпример₁

? 2 1 3

max = 2

 

Но этот результат - неправильный. Следовательно, алгоритм и программа содержат ошибки. Но сколько этих ошибок - одна, две, а может быть больше?

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

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

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

В качестве примера проведем анализ результатов алгоритма, со­стоящего из трех присваиваний.

алг «у = х⁵» РезультатыУтверждения

Нач

v:= х×х v₁ = х×х Þ v₁ = x²

v:= v×v v₂ = v₁×v₁ Þ v₂ = x⁴

у:= v×x у = v₂×x Þ у = х⁵

Кон

 

Справа от алгоритма приведены результаты выполнения присва­иваний. Результатом первого присваивания v:= х×х будет значение v₁ = х×х переменной v. Результат следующего присваивания v:= v×v - второе значение переменной v, равное v₂ = v₁×v₁. Результатом треть­его присваивания у:= v×x будет значение у = v₂×x.

На основе приведенных рассуждений, можно сделать три утверж­дения о промежуточных и конечных результатах вычислений:

РезультатыУтверждения

{ v₁ = х×х Þ v₁ = х²

{ v₂ = v₁×v₁ Þ v₂ = x⁴

{ у = v₂×x Þ у = х⁵

 

Таким образом можно высказать окончательное

Утверждение. Конечным результатом выполнения будет

у = х⁵ для любых значений х.

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

 

у = v₂×x = (v₁×v₁)×x = ((х × х).(х × х))) × х = x⁵.

Что и требовалось доказать.

 

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

· разбор случаев;

· подбор контрпримеров;

· выделение лемм;

· индуктивный вывод.

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

 

алг «у = тах(а, b,с)» Результаты

Нач

если а > b то при а > b

у:= а у = а

инес b > с то при b > с

у:= b у = b

инес с > а то при с > а

у:= с у = с

кесли при не (b > с)

Кон

 

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

 

а, при а > b,

у = b, при b > с и b ³ а,

с, при с > а и с ³ b.

 

В то же время значение максимума должно быть равно:

 

а, при а ³ b и а ³ с,

mах = b, при b ³ с и b ³ а,

с, при с ³ а и с ³ b.

 

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

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

Контрпримером в данном случае будут значения: а = 2, b = 1, с = 3. Для этих данных по определению mах = 3, а по результатам выполнения алгоритма у = 2. Следовательно, в алгоритме содержится ошибка.

Однако оказывается, что это не единственная ошибка. Более тон­кие ошибки вскрывает второй контрпример: а = 1, b = 1, c = 1. Для этих данных в алгоритме вовсе не определен результат вычислений у =? и конечный результат выполнения программы будет непред­сказуем!?

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

Постановка задачиМетод решения

Вычисление mах (а, b, с).

Дано: а, b, с - три числа. mх = mах(mах(а,b),с)

Треб.: mх – максимум. mах(х,у) = х, при х ³ у

Где: mх = mах (а, b, с). у, при у ³ х

 

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

 

алг «тх = тах(а,b,с)» Результаты

Нач

если а ³ b то при а ³ b

тх : = а mx = a

иначе при b > а

mх : = b mх = b

кесли { mх = mах(а,b) } при с < mх

если с ³ mх то при с ³ mх

mх:= с mх' = с

Кесли

Кон

Доказательство правильности алгоритмов можно проводить двумя способами. Первый способ - анализ правильности при по­строении алгоритмов. Второй способ - анализ правильности после построения алгоритмов.

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

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

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

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

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

Лемма: Конечными результатами выполнения алгоритма

АлгоритмРезультаты

если а > b то при а ³ b

тх := а mx = a

иначе при b > a

тх:= b mx = b

Кесли

 

является значение mx = max(а, b) для любых значений а и b.

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

 

а при а ³ b

mx =

b при а < b

 

что совпадает с определением max (а, b).

С помощью этой леммы легко доказать правильность алгоритма в целом.

 

{ mх = max (а, b) } Результаты

если с ³ mx то при с ³ mx

mx:= с mx' = с

кесли mx' = mx

при с < mx

 

Утверждение. Конечным результатом выполнения алгоритма вы­числения максимума будет значение mx' = max (а, b, с) для любых значений а, b и с.

Доказательство. В силу предположения предшествующее значе­ние переменной mx = max(a,b). Отсюда получаем, что

 

с, при с ³ mx

mx¢ = = max(a,b,c).

mx, при с < mx

Что и требовалось доказать.

Доказательство лемм - основной прием доказательства правиль­ности сложных алгоритмов и программ. Напомним, что лемма — это вспомогательное утверждение, предполагающее отдельное доказа­тельство.

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

В качестве примера использования индуктивных рассуждений рассмотрим алгоритм вычисления среднего арифметического после­довательности чисел. В приводимом алгоритме предполагается, что последовательность чисел размещена в массиве X[1:N].

 

Алг «среднее значение»

массив X[1:N]

нач Результаты:

от k = 1 до N цикл

S:= S * (k-l)/k + X[k]/k S_k = S_k-1*(k-l)/k + X[k]/k

кцикл [k = (1...N)]

Xcp:= S Xcp = S

Кон

 

Этот алгоритм обычно считается ошибочным (?!). «Ошибкой» в этом алгоритме считается отсутствие присваивания S:= 0 перед началом цикла.

Разберем результаты выполнения алгоритма на первых трех ша­гах:

 

S₁ = S₀×(l - 1)/1 + Х[1]/1 = S₀×0/1 + Х[1]/1 = Х[1]/1;

S₂ = S₁×(2 - 1)/2 + Х[2]/2 = S₁×1/2 + Х[2]/2 = Х[1]/2 + Х[2]/2;

S₃ = S₂×(3 - 1)/3 + Х[3]/3 = S₂×2/3 + Х[3]/3 = Х[1]/3 + Х[2]/3 + Х[3]/3.

 

Можно утверждать, что на первых трех шагах результатом является среднее арифметическое обрабатываемых чисел. На основе этих примеров можно сделать индуктивное утверждение - «на каждом очередном k-м шаге выполнения цикла результатом будет среднее арифметическое»

 

S_k = S_k-1×(k-l)/k + X[k]/k = X[l]/k + X[2]/k +... + X[k]/k.

 

Доказательство этого утверждения проводится с помощью мате­матической индукции. На первом шаге при k = 1 оно уже доказано. Допустим, что оно справедливо на (k -1)-м шаге

 

S_k-1 = X[l]/(k-l) + X[2]/(k-l) +... + X[k-l]/(k-l).

 

Подставим его в описание результатов цикла на k-м шаге

 

S_k= S_k-1×(k-l)/k +X[k]/k.

 

Тогда результат выполнения цикла на k-м шаге оказывается рав­ным

 

S_k = X[l]/k + X[2]/k +... + X[k-l]/k + X[k]/k,

 

т. е. среднему арифметическому первых k чисел.

Таким образом, индуктивное утверждение доказано. В силу мате­матической индукции это утверждение верно для всех k = l, 2,..., N. Следовательно, на последнем шаге конечным результатом выполнения цикла станет значение

 

S_N = S_N-1×(N-1) + X[N]/N = X[1]/N +... + X[N]/N.

 

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

 

Xcp = S_N = X[1]/N +... + X[N]/N.

 

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

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

Математическая индукция - это принцип доказательства после­довательностей утверждений Р(1), Р(2), Р(3),..., P(N),.... когда известно, что верны первые утверждения для n = 1, 2, 3 и из истин­ности (n - 1)-го утверждения следует истинность n-го утверждения:

Принцип математической индукции: если первое утверждение Р(1) истинно и из утверждения Р(n - 1) следует утверждение Р(n), то истинны все утверждения Р(1), Р(2), Р(3),..., Р(n),....

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

 

Алг «нахождение минимума»

массив x[1:N]

нач Результаты:

от k = 1 до N цикл

если x[k] < min то

тп:= x[k] mn_k = { x[k], при x[k] < mn_k-1

все { mn_k-1, в ином случае

кцикл [ k = (1... N)]

Min:= тп Min = mn_N

Кон

 

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

Доказательство. Для демонстрации ошибок необходимо привести контрпример. Для построения контрпримера разберем результаты выполнения на первом шаге цикла.

Результаты выполнения первого шага цикла при k = 1:

 

х[1] при х[1] < mn₀

mn₁ = = min (х[1], mn₀).

mn₀ при х[1] £ mn₀

 

Следовательно, результатом будет

 

mn₁ = min (x[l], mn₀).

 

Однако поскольку начальное значение mn₀ неизвестно, то не­определено значение результата выполнения первого шага цикла. Аналогичное утверждение можно сделать о втором и всех последу­ющих шагах выполнения цикла:

 

mn_k = min (x[k], Min(x[k-l],..., х[1], mn₀) = Min (x[k], x[k-1],..., х[1], mn₀).

 

В силу математической индукции это утверждение справедливо при k = N:

 

mn_N = Min (x[N], x[N - 1],..., x[2], х[1], mn₀).

 

Таким образом на основании этого утверждения можно сделать заключение о конечном результате выполнения алгоритма в целом:

 

Min = mn_N = Min (x[N], x[N - 1],..., x[2], х[1], mn₀).

 

Из этой формулы видно, что конечный результат равно как и результат первого присваивания зависит от начального значения mn₀ переменной mn. Однако эта величина не имеет определенного значения, соответственнно неопределен и конечный результат выполнения алгоритма в целом, что и является ошибкой.

В самом деле, если значение mn₀ окажется меньше любого из значений последовательности х[1],.... x[N], то конечный результат вычислений будет неправильным. В частности, при реализации алгоритма на Бейсике неправильный результат будет получен, если последовательность будет состоять только из положительных чисел. Например, для последовательности чисел: 1, 2, 3,..., N.

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

 

алг «нахождение минимума» массив х[1:п] нач тп:= x[1] от k = 1 до N цикл если x[k] < тп то тп = x[k] все кцикл Min = тп кон

Результаты: mn0 = х[1] [k = (1... N)] Min = mnN

 

Утверждение. Для любой последовательности чисел x[l:N] конечным результатом вычислений будет значение Min = Min (х[1],..., x[N]).

Доказательство. Воспользуемся результатами анализа выполнения алгоритма, рассмотренного ранее. Различие между ними состоит в добавлении перед началом цикла присваивания mn:= х[1], которое задает начальное значение переменной mn, равное mn₀ = х[1].

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

 

Min = mn_N = Min(x[N], x[N-l],..., х[2], х[1], mn₀) =

= Min(x[N], x[N-l],..., x[2], x[l], x[l]) = Min(x[N],.... х[1]).

Что и требовалось.

Рассмотренные примеры являются образцами доказательств пра­вильности алгоритмов и программ, которые могут использоваться для анализа и доказательства правильности других новых алгоритмов и программ обработки данных.

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

 

Вопросы

1. Как показать наличие ошибок в алгоритме?

2. Сколь долго может продолжаться отладка программ?

3. Зачем нужны доказательства в анализе алгоритмов?

4. Из чего состоит техника доказательств правильности?

5. Когда применяется разбор случаев?

6. Что такое леммы?

7. Что такое индуктивные рассуждения?

 

Адания

1. Приведите постановку, алгоритм решения и разбор правильности для следующих задач:

а) подсчет суммы целых чисел;

б) подсчет суммы нечетных чисел;

в) подсчет членов арифметической прогрессии;

г) подсчет членов геометрической прогрессии.

2. Для последовательности чисел х₁, х₂,..., х_N, приведите постановку, алгоритм решения и разбор правильности следующих задач:

а) подсчет суммы всех чисел;

б) вычисление среднего арифметического чисел;

в) определение наибольшего из чисел;

г) определение наименьшего из чисел.

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

а) нахождение самого высокого ученика;

г) нахождение самого легкого ученика;

д) нахождение среднего роста учеников;

е) нахождение суммарного веса учеников.

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

а) подсчет сумм элементов матрицы по столбцам;

б) нахождение минимального значения в каждом столбце;

в) нахождение максимального значения в каждой строке;

г) нахождение наибольшего из минимальных значений в столбцах;

д) нахождение наименьшего из максимальных значений в строках.

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

а) найти точку, наиболее удаленную от центра координат;

б) соединить пару наиболее удаленных точек;

в) найти три точки, образующие треугольник с наибольшим пери­метром;

г) найти три точки, образующие треугольник с наибольшей пло­щадью.

 

Решение сложных задач

 

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

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

Анализ правильности сложных алгоритмов и программ распадается на анализ правильности каждого из вспомогательных алгоритмов и на анализ правильности программ в целом. Необходимым условием для этого является составление спецификаций для каждого из вспомо­гательных алгоритмов и каждой подпрограммы.

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

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

Первая задача: упорядочение массивов данных. Пример, для чисел 3, 7, 9, 1, 4 упорядоченная последовательность имеет вид: 1, 3, 4, 7, 9.

Существует несколько способов и методов упорядочения масси­вов и последовательностей. Простейший из них называется методом «пузырька».

Метод «пузырька» состоит в нахождении в массиве наименьшего числа и перестановке его на первое место. Это как бы «пузырек», поднимающийся к началу массива. Затем в остатке массива нахо­дится наименьшее число, которое перемещается на второе место, и так далее - до исчерпания всего массива.

Для рассматриваемых чисел метод «пузырька» дает следующие перестановки:

исходные числа: 3, 7, 9, 1, 4.

перестановка₁: 1, 7, 9, 3, 4.

перестановка₂: 1, 3, 9, 7, 4.

перестановка₃: 1, 3, 4, 7, 9. упорядочено.

 

Приведем точную математическую постановку задачи.

Постановка задачи

Упорядочение последовательности чисел.

Дано: x₁, х₂,..., х_N - исходные числа.

Треб.: x₁', x₂',..., х_N' - упорядоченные числа.

Где: х₁' £ х₂' £... £ х_N'.

При: N > 0.

Упорядочение чисел по методу «пузырька» в общей форме имеет вид:

Способ «упорядочение чисел»

нач

от k=1 до N-1 цикл

хтп:= xk

imn:= k

от i=k+1 до N цикл

если xi < хтп то

хтп:= xi

imn: = i

кесли

кцикл

xmn = Min (х_k,..., х_N)

xk' = хтп

ximn ' = xk

кцикл х_k¢ = Min (х_k,..., х_N)

кон x₁ < х₂ <... < х_k¢

 

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

Первый фрагмент (внутренний цикл) решает подзадачу нахожде­ния минимального значения в подмассиве x[k:N]. Второй фрагмент решает подзадачу перемещения k-го минимального значения на k-e место в массиве.

Лемма 1. Для вспомогательного алгоритма

Алг «поиск минимума»

Нач

хтп:= xk

imn:= k

от i = k + 1 до N цикл

если x_i < хтп то

хтп:= x_i

imn:= i

Кесли

кцикл { xmn = Min (х_k,..., х₁) }

Кон

 

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

 

xmn = Min (х_k,..., х_N).

Доказательство. Применим индуктивную схему рассуждений. Первое присваивание дает

 

xmn_k = x_k.

 

Далее на первом шаге цикла при i = k + 1 будет получен минимум первых двух чисел:

 

x_k+1 при x_k+1 < xmn_k,

xmn_k+l =

xmn_k при x_k+1 ³ xmn_k.

 

На втором шаге цикла будет получен минимум первых трех чисел:

 

xmn_k+2 = min (x_k+2, min (х_k+1, х_k)) = Min (х_k+2, х_k+1, х_k).

 

Теперь можно утверждать, что на третьем и последующих шагах цикла результатом будет минимальное значение среди чисел xk,..., xi

 

хmn_i = Min (х_k,..., х_i).

 

Данное утверждение доказывается с помощью математической индукции. На первых двух шагах при i = k + 1, k + 2 оно уже уста­новлено. Покажем, что оно будет выполняться на (i + 1)-м шаге. Действительно, на следующем шаге цикла результатом будет:

 

x_i+1 при х_i+1 < xmn_i = min(x_i+1, хmn_i)

хmn_i+1 =

хmn_i при х_i+1 ³ хmn_i = min(x_i+1, xmn_i)

= min (x_i+1, Min (х_k,..., х_i)) = Min (х_k,..., х_i, x_i+1).

 

Что и требовалось показать. Следовательно, в силу принципа мате­матической индукции конечным результатом выполнения рассмат­риваемого цикла будет значение:

 

xmn_N = Min (x_k, ..., х_N)

Что и требовалось доказать.

Лемма 2. Для вспомогательного алгоритма

Алг «перестановки»

нач { xmn = Min (х_k,..., х_N) }

x_i¢_mn= x_k

Кон

 

конечным результатом будет значение х_k' = Min (х_k,..., х_N).

Доказательство. В силу леммы 1 xmn = Min (x_k,..., х_N). А так как в этом алгоритме х_k' = xmn, то в итоге получим

 

х_k' = xmn = Min (х_k,..., х_N).

Что и требовалось.

Утверждение. Конечным результатом выполнения алгоритма будет упорядоченная последовательность чисел х₁',..., х_N', удовлет­воряющая условию х₁' £ х₂' £... £ х_N'.

Доказательство проводится по индуктивной схеме рассуждений. Рассмотрим результаты выполнения основного цикла основного алгоритма:

Алг «упорядочение чисел»

Нач

от k = 1 до N - 1 цикл

xmn:=х_k

............... { xmn = Min (х_k,..., х_i) }

х¢_k = xmn_N

хmп¢ = х_k

кцикл { х_k' = Min (х_k,..., х_N) }

кон { х₁' £ х₂' £... £ х_k' }

 

На первом шаге при k = 1 первый элемент последовательности

 

х₁' = Min (x₁, х₂,..., х_N),

 

На втором шаге второй элемент последовательности

 

x₂' = Min (х₂,..., х_N).

 

В силу свойств минимума последовательности чисел будем иметь

 

х₁' = Min(x₁, x₂,..., х_N) = min (x₁, Min (х2,..., хN) £ (Min (х2,..., хN) = x₂'.

 

Таким образом, при k = 2 результатом станут значения х₁' и x₂', такие что

 

х₁' £ x₂'

 

На третьем шаге выполнения основного цикла результатом станет

 

х₃ = Мin(х₃,..., х_N).

 

Опять же в силу свойств минимума последовательности имеем

 

х₂' = Min (х₂, х₃,..., х_N) = min (x₂, Min (x₃,..., х_N)) £ Min (x₃,..., х_N) = x₃'.

 

Таким образом, после третьего шага при k = 3 первые три значе­ния последовательности х₁', x₂', x₃' будут удовлетворять условию

 

х₁'£ x₂'£ x₃'

 

Из приведенных выкладок можно сделать индуктивное предположение, что на каждом очередном k-м шаге выполнения основного цикла первые k членов последовательности х₁', x₂',.... х_k' будут удов­летворять условию

 

х₁'£ x₂'£ … £ x_k'.

 

Данное предположение доказывается с помощью математической индукции. На начальных шагах при k = 2 и k = 3 оно уже показано. Покажем, что оно будет выполнено на (k + 1)-м шаге, если это усло­вие выполнено на k-м. шаге.

В силу леммы 2 на k-м и (k + 1)-м шагах выполнения основного цикла промежуточными результатами будут

 

х_k' = Min(x_k, x_k+1,..., х_N),

х_k+1' = Min (x_k+1,..., х_N).

 

В силу свойств минимума последовательности чисел имеем

 

х_k' = Min(x_k, x_k+1,..., х_N) = min (х_k, Min (х_k+1,...,х_N)) £ Min (x_k+1,..., х_N) = х_k+1'.

 

Таким образом, х_k £ x_k+1 и в силу индуктивного предположения получаем, что

 

x₁' £ х₂' £... £ х_k' £ x_k+'₁.

Что и требовалось доказать.

 

Осталось уточнить результаты выполнения последнего шага цикла при k = N - 1. В силу леммы 2 результатом будет значение

 

x_N-'₁ = Min (x_N-1, x_N) £ х_N'.

 

Таким образом, после N - 1 шагов выполнения основного цикла для последовательности в целом будут выполнены соотношения упорядоченности

 

x₁' £ x₂' £... £ х_N'.

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

 

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

Данные о товарах представлены двумя таблицами:

 

Товар стоим кол-во

яблоки
огурцы
арбузы

 

Товар цена остаток

яблоки
огурцы
арбузы

 

Приведем точную постановку задачи и сценарий диалога с ком­пьютером для решения поставленной задачи.

Постановка задачиСценарий

Сортировка товаров по остатку.

Дано: товары:

D = (d₁, d₂,.... d_N) - данные товара, <товар₁> <s₁> < m ₁> *

d = (товар, s, m),............

s - стоимость, m - кол-во, остатки:

R = (r₁, r₂,..., r_N) - данные об остатках, <товap₁> <c₁> < р₁> *

г = (товар, с, р),............

с - цена, р - остаток.

Треб.: S - сумма выручки, выручка = <S>

R' = (r₁',..., r_N') - упорядоченные данные, сортировка:

Где: <товар₁'> <с₁'> <р₁'> *

S = (c₁-s₁)×(m₁-p₁) +...+ (с_N-s_N)×(m_N-р_N),............

р₁' £ р₂' £... £ р_N',

р_k' = р_i для k = 1... N и i = 1... N.

При: N > 0.

 

Для представления исходных данных в программе примем опера­торы data:

 

tovs: 'товары: osts: 'остатки: