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

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

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

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

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

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

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

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

,

если путь из i в j проходит по ветви, отмеченной T (истина), и

,

если путь из i в j проходит по ветви, отмеченной буквой F (ложь). Через path’ обозначается часть пути из i в j от точки i до точки m. Теперь образуем полное высказывание . Запишем формализованное условие верификации для пути из точки i в точку j:

[А_i (Х, Y, ...)  С _path]  А_j [e _path (Х), e _path (Y), ...).

Если на пути не встречаются проверки, то С _path высказывание не включается.

Пример 2.1. Рассмотрим блок-схему (рис. 2.1). Для записи утверждений, относящихся к разным точкам блок-схемы, использована нотация исчисления предикатов.

Сформируем множество условий верификации.

1. Путь из точки 1 в точку 2 назовем р1. Для этого пути имеем е_р1 (J1) = J1, е_р1 (J2) = J2, е_р1 (IQ) = 0, е_р1 (IR) = J1. Так как по пути проверки не выполняется, то можно написать следующее условие верификации для этого пути:

(0  J1  1  J2)  [е_р1 (J1) = е_р1 (IQ)  е_р1 (J2) + е_р1 (IR)  0  е_р1 (IR)],

( 0  J1  1  J2 )  ( J1 = IQ  J2 + J1  0  J1).

2. Путь из точки 2 через точки 3, 4 в точку 2 обозначим через р2. Для этого пути имеем е_р2 (J1) = J1, е_р2 (J2) = J2, е_р2 (IQ) = IQ + 1, е_р2 (IR) = IR – J2.

На пути есть только одна проверка IR < J2. Ту часть пути р2, которая ведет от точки 2 до этой проверки, обозначим через р2'. Так как путь р2 после проверки проходит по ветви, отмеченной F, то

.

Поскольку проверка только одна, получаем

С_p2   t^p2.

Отсюда условие верификации для этого пути имеет вид

( J1 = IQ  J2 + IR  0  IR  J2  IR )   [е_р2 (J1) = е_р2 (IQ)  е_р2 (J2) + е_р2 (IR)  0  е_р2 (IR)],

или после преобразования

(J1 = IQ  J2 + IR  0  IR  J2  IR)  [J1 = (IQ + 1)  J2 + (IR – J2)  0 < IR – J2].

Рис. 2.1

3. Путь из точки 2 через 5 в точку 6 обозначим через рЗ. Для этого пути имеем е_р3 (J1) = J1, е_р3 (J2) = J2, е_р3 (IQ) = IQ, е_р3 (IR) = IR. На пути встречается лишь одна проверка IR < J2.

Часть пути от точки 2 до этой проверки обозначим через р3'. Как и выше, имеем е_р3' (IR) = IR и е_р3' (J2) = J2. Так как после проверки путь проходит по ветви, обозначенной Т (истина), то

.

Следовательно, условие верификации для всего пути имеет вид

(J1 = IQJ2+IR  0IR  IR<J2)  (J1 = IQJ2+IR  0<IR  IR<J2).

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

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

6. Доказательство правильности программ, написанных на языках программирования. Отличия от доказательства правильности блок-схем. Доказательство правильности программ, содержащих обращение к подпрограммам.

Методы доказательства правильности программ. К неформальным методам доказательства правильности программ относят отладку и тестирование, которые являются необходимой составляющей на всех этапах процесса программирования, хотя и не решают полностью проблемы правильности. Существенные ошибки легко найти, если использовать приемы отладки (контрольные распечатки, трассировки). Тестирование - процесс выполнения программы с намерением найти ошибку, а не подтвердить правильность программы.. Метод установления правильности программ при помощи строгих средств известен как верификация программ. В отличие от тестирования программ, где анализируются свойства отдельных процессов выполнения программы, верификация имеет дело со свойствами программ. В основе метода верификации лежит предположение о том, что существует программная документация, соответствие которой требуется доказать. Документация должна содержать следующие спецификации: • спецификация ввода-вывода (описание данных, не зависящих от процесса обработки); • свойства отношений между элементами векторов состояний в выбранных точках программы; • спецификации и свойства структурных подкомпонентов программы; • спецификация структур данных, зависящих от процесса обработки. К такому методу доказательства правильности программ относится Метод индуктивных утверждений. Суть этого метода состоит в следующем: 1) формулируются входное и выходное утверждения: входное утверждение описывает все необходимые входные условия для программы (или программного фрагмента), выходное утверждение описывает ожидаемый результат; 2) предполагая истинным входное утверждение, строится промежуточное утверждение, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями); такое утверждение называется выведенным утверждением; 3) формулируется теорема (условия верификации): из выведенного утверждения следует выходное утверждение; 4) доказывается теорема; доказательство свидетельствует о правильности программы (программного фрагмента). Доказательство проводится при помощи хорошо разработанных математических методов, использующих исчисление предикатов первого порядка. Условия верификации можно построить и в обратном направлении, т.е., считая истинным выходное утверждение, получить входное утверждение и доказывать теорему: из входного утверждения следует выведенное утверждение. Такой метод построения условий верификации моделирует выполнение программы в обратном направлении. Другими словами, условия верификации должны отвечать на такой вопрос: если некоторое утверждение истинно после выполнения оператора программы,то какое утверждение должно быть истинным перед оператором? Самым сложным в процессе доказательства является построение индуктивных утверждений. Это объясняется, во-первых,тем, что необходимо описать все содержательные условия, и, во-вторых, тем, что необходимо аксиоматическое описание семантики языка программирования. Таким образом, алгоритм доказательства правильности программы методом индуктивных утверждений представляется в следующем виде.

Описание алгоритма. 1) Построить структуру программы. 2) Выписать входное и выходное утверждения. 3) Сформулировать для всех циклов индуктивные утверждения. 4) Составить список выделенных путей. 5) Построить условия верификации. 6) Доказать условие верификации. 7) Доказать, что выполнение программы закончится. Преимущество верификации состоит в том, что процесс доказательства настолько формализуем, что он может выполняться на вычислительной машине. Для автоматизированной диалоговой системы программист должен задать индуктивные утверждения на языке исчисления предикатов. Синтаксис и семантика языка программирования должны храниться в системе в виде аксиом на языке исчисления предикатов. Система должна определять пути в программе и строить условия верификации. Основной компонент доказывающей системы - это построитель условий верификации, содержащий операции манипулирования предикатами, алгоритмы интерпретации операторов программы. Вторым компонентом системы является подсистема доказательства теорем, что относится к области искусственного интеллекта. ОСНОВНЫЕ ПРИНЦИПЫ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ ДЛЯ БЛОК-СХЕМ

Если мы хотим доказать, что некоторая программа пра­вильна или верна, то прежде всего должны уметь описать то, что по предположению делает эта программа. Назовем такое описание высказыванием о правильности или просто утвержде­нием. В этом случае доказательство правильности состоит из доказательства того, что программа, будучи запущенной, в конце концов окончится (выполнится оператор STOP), и после окончания программы будет справедливо утверждение правильности. Часто требуется, чтобы программа работала правильно только при определенных значениях входных данных. В этом случае доказательство правильности состоит из доказательства того, что если программа выполняется при соответствующих входных данных, то она когда-либо за­кончится, и после этого будет справедливо утверждение о правильности.

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

ПРИМЕР 1. Предположим, что нужно вычислить произ­ведение двух любых целых чисел М, N, причем М>0 и операцию умножения использовать нельзя. Для этого можно использовать операцию сложения и вычислить сумму из М слагаемых (каждое равно N). В результате получим М • N. Рассмот­рим блок-схему, реализующую такое вычисление (рис. 2.1). Нужно доказать, что приведенная программа правильно вычисляет произведение двух любых целых чисел М и N при условии М>0, т. е. если программа выполняется с целыми числами М и N, где М>0, то она в конце концов окончится (достигнув точки 5) со значением J = M -N.

Чтобы удостовериться в правильности работы блок-схемы, можно было бы проверить ее с некоторыми фиксированными данными. Например, давайте «вручную» промоделируем выполнение программы с числами М=3 и N=5. Ниже при­ведены значения переменных I и J в моменты достижения точки 2 на блок-схеме (вход в цикл):

Число проходов n через точку 2 Значение I Значение J

при выполнении блок-схемы

1 0 0

2 1 5

3 2 10

4 3 15

Когда мы в четвертый раз дойдем до точки 2, значение

I= 3, т. е. равно М, поэтому выполнение цикла закончится и, мы попадем в точку 5.

При попадании в точку 5 переменная J = 15 =3*5. Таким образом, мы убеждаемся, что при М =3 и N = 5 блок- схема работает верно. Хотя это, конечно, и укрепляет нашу уверенность в правильности работы программы, но тем не менее никак не доказывает, что программа будет работать правильно при всех возможных значениях М и N. Можно продолжать проверять программу с другими значениями М и N. Если для некоторых значений М и N будет получен неверный ответ, то надо еще узнать, что он неверен. Однако, если мы даже будем продолжать получать правильные ответы, все равно не будем уверены, что такие ответы будут полу­чаться для любых возможных значений М и N. Всегда остается бесконечное число возможных значений, для которых про­грамма еще не проверялась. Конечно, если речь идет о неко­торой конкретной машине, то значение М и N ограничены некоторым конечным интервалом для целых чисел. В прин­ципе в этом случае можно провести исчерпывающую проверку с числами в этом интервале. Однако для большинства машин этот интервал настолько велик, что проводить исчер­пывающую проверку было бы не практично. Кроме того, мы составляем программу обычно таким образом, чтобы она работала верно независимо от размеров N и М. Следовательно, мы будем удовлетворены лишь тогда, когда сможем показать, что программа работает правильно независимо от размеров М и N. Методом тестирования мы этого никогда не достигнем.

Предположим, что вместо выполнения программы с кон­кретными значениями М и N мы начнем ее выполнять с символическими данными М и N. В этом случае мы получим следующую «трассу» для значений I и J при проходах через точку 2:

Число проходов п Значение I Значение J

1. О О

2. 1 N ,

3. 2 2 • N

4. 3 3 • N

М+1 М М • N

Видно, что при выполнении цикла М раз (т. е. при М + 1-ом попадании в точку 2) I⁼M, a J=M*N. Так как 1=М, то мы покидаем цикл и попадаем в точку 5. Таким образом, при достижении точки 5 работа программы заканчи­вается и мы получаем J = М • N. Это показывает, что про­грамма правильно работает для любых значений М и N. Однако отметим, что наша трассировка предполагает, что М>0, и поэтому значение I в конце станет равным М (оно начинается с 0 и увеличивается на 1 при каждом про­хождении цикла). Если М < 0, то цикл будет повторяться, а значение I никогда не станет равным М; следовательно, программа не сможет закончиться. Таким образом, блок- схема в действительности работает правильно' только для М >0. При любых целых значениях М и N и при условии М >0, как это видно из проведенной трассировки, работа блок-схемы закончится с J. =М • N.

Все это доказывается методом индукций.

ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ, НАПИСАННЫХ НА ОБЫЧНЫХ ЯЗЫКАХ ПРОГРАММИРОВАНИЯ

Метод индуктивных утверждений, можно непосредственно использовать для доказательства частичной правильности программ, написанных на каком-нибудь традиционном языке програм­мирования, например на Фортране, Алголе или ПЛ/1. Конечность таких программ можно доказывать так же, как мы это делали для блок-схем. При использовании метода индуктивных утверждений необходимо по крайней мере с одной из точек программы в каждом из замкнутых путей (циклов) связать соответствующее утверждение. Конечно, если мы используем язык программирования, то порядок выполнения (пути) неявно определяется структурой управ­ления, тогда как на блок-схемах этот порядок явно указывается стрелками. Следовательно, применяя метод индуктивных утверждений, нужно четко представлять порядок выполнения программы, чтобы быть уверенным, что не пропущен ни один из замкнутых путей в программе. Именно этот вопрос мы и рассмотрим здесь.

ПРИМЕРЫ ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ ПРОГРАММ НА ФОРТРАНЕ

READ (5, 1) Jl, J2

1. FORMAT (2I10)

С ЗНАЧЕНИЯ, СЧИТЫВАЕМЫЕ В J1 И J2,-

С ЦЕЛЫЕ, УДОВЛЕТВОРЯЮЩИЕ УСЛОВИЯМ С О.LE. J1 И 1 .LE. J2.

IQ-0

IR = JI

5. IF (IR .IT, J2) GO TO 4

С Jl .EQ. IQ * I2 + IR AND 0 .LE. IR

IQ=IQ + 1

IR = IR - J2

3. GO TO 2

4. , WRITE (6,5) IQ, IR

5. FORMAT (2I10)

С Jl .EQ. IQ * J2 + IR AND 0 .LE. IR AND

С IR .LT, J2

STOP ,

END

Приведенная программа на Фортране — это просто некото­рый вариант программы, блок-схема которой приведена на рис. 2.3. Напомним, что программа вычисляет целое частное IQ и остаток IR от деления целого J1 на целое J2. Мы уже включили в качестве комментариев в программу индуктивные утверждения, необходимые для доказательства частичной правильности. Например, комментарий, помещенный сразу после оператора с меткой 2, нужно рассматривать как коммен­тарий, связанный с точкой, расположенной перед выполня­емой в этом операторе проверкой. Таким образом, предпо­лагается, что в момент прихода в точку, находящуюся непо­средственно перед проверкой в операторе с меткой 2, спра­ведливы утверждения Jl =IQ • J2 + IR и 0< IR. Отметим, что в доказательствах мы используем „ =“ как символ равенства, а не присваивания.

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

Путь от оператора READ до оператора с меткой 2.

Предположим, что только что выполнился оператор READ и справедливо утверждение, записанное сразу после него. Теперь последовательно выполняются операторы до опера­тора с меткой 2. Нам нужно показать, что справедливо

утверждение, записанное после этого оператора. Если мы дошли до этой точки, то имеем IQ = О, IR = J1,0 < J1 и 1< J2. Таким образом,

J1 = IQ * J2 + IR =0 • J2 + J1 =J1 и 0< J1 =IR

Следовательно, наше утверждение справедливо.

Путь от оператора с меткой 2 до оператора с меткой 3 и опять к оператору с меткой 2 (основной цикл программы). Предположим, что мы выполняем оператор 2 и справедливо записанное после него утверждение, затем выполняем цикл и возвращаемся к метке 2. Необходимо показать, что указанное утверждение снова будет справедливо. Пусть IQ и IR до выполнения цикла принимают значения IQ_n и IR_n. Тогда J1=IQn • J2 + IR_n и 0<IR_n. При возврате к метке 2 после прохождения цикла значения IQ и IR будут IQ_n+1 = IQ_n +1 и IR_n+1 =IR_n-J2, а значения J1 и J2 останутся без изменений. Таким образом, после возврата к метке 2 имеем

IQ_n+1 • J2 + IR_n+1 = (IQ + 1) • J2 + (IR_n - J2) = IQ_n* J2 + J2 + IRn-J2=IQ_n*J2 + IRn= Jl.

Кроме того, известно, что если мы проходили по циклу, то проверка IR_n .LT. J2 дала отрицательный результат, т. е. J2<IR. Отсюда следует, что при возврате к метке 2 имеем 0 < IR_n^—J2 = IR_n+1.

Путь от оператора 2 к оператору 4. Предположим, что мы выполнили оператор 2, справедливо соответствующее утверждение и переходим к оператору 4. Нужно показать, что справедливо утверждение, записанное ниже этого опе­ратора. Оператор 2 передаст управление на оператор 4 только при положительном результате проверки IR .LT. J2. При переходе от оператора 2 к оператору 4 ни одно из значений переменных не изменяется, и, следовательно, при достижении метки 4 мы имеем J1 =IQ • J2 + IR, 0<IR и, кроме тога, IR < J2. Таким образом, мы доказали частичную правильность.

Доказательство конечности программы на Фортране иден­тично доказательству конечности для блок-схем. Для дока­зательства конечности программы необходимо только пока­зать, что при выполнении программы мы в конце концов выйдем из единственного в программе цикла. Следовательно, надо показать, что проверка IR .LT. J2, управляющая циклом, когда-нибудь даст положительный результат. Так как значе­ние IR при каждом прохождении цикла уменьшается на вели­чину J2, a J2 остается без изменений и, кроме того, 1< J2, то можно заключить, что IR уменьшается каждый раз по крайней мере на 1 и когда-нибудь станет меньше J2. В этот момент условие IR< J2 станет справедливым и мы выйдем из цикла, т. е. программа закончится.

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

ПРИМЕР 3

С MAIN PROGRAM

.

.

.

.

Cl 0 .LE. I AND 1 .LE. J AND A(I, J)

CALL DIV(I, J, K, L)

С2 О lЕ. I AND 1 .LE. J AND A(I, J)

C2 AND I ,EQ.K*J + L AND О .LE. L AND I .LT.

.

.

.

.

END

SUBROUTINE DIV (Jl, J2, IQ, IR)

C3 0 .LE. Jl AND 1 .LE, J2

IR=J1

2. IF (IR LT. J2) GO TO 4

C4 Jl .EQ .IQ*J2 + IR AND 0 LE. IR

IQ=IQ+1

IR = IR-J2

2. GO TO 2

3. RETURN

C5 Jl ,EQ. IQ * J2 + IR AND 0 .LE. IR AND IR lT. J2

END

В этом примере нас прежде всего будет интересовать, как обрабатывать подпрограммы. Поэтому мы не приводим целиком основную программу, а лишь намечаем некоторую программу, содержащую обращения к подпрограммам. Подпрограмма DIV. Она предназначена для вычи­сления целых частного и остатка от деления параметра J1 на параметр J2; полученные значения возвращаются как значения параметров IQ и IR. Один из этапов такого доказательства заключается в том, чтобы показать, что если непосредственно перед обращением к подпрограмме спра­ведливо утверждение С1, а затем мы пройдем эту точку, выполним подпрограмму и вернемся из нее, то будет справед­ливо утверждение С2. Мы считаем, что A(I, J) в примечаниях С1 и С2 — некоторые утверждения, относящиеся к перемен­ным I и J. Чтобы доказать этот факт, мы поступим следую­щим образом. Так как фактические параметры I, J, К, L с помощью механизма обращения сопоставляются с соответст­вующими формальными параметрами Jl, J2, IQ, IR, то сначала следует доказать, что из утверждения С1 следует утверждение СЗ в начале подпрограммы; для этого имена параметров Jl, J2, IQ и IR в этом утверждении заменяются на имена соответствующих фактических параметров I, J, К, L. Другими словами, нужно доказать, что С1 подразумевает СЗ', где СЗ' — утверждение, полученное путем замены в СЗ J1 на I, J2 на J, IQ на К и IR на L. Таким образом, нужно показать, что из

.LE. I, 1 .LE. J и A(I, J) следует О .LE. I и 1 .LE. J. Это очевидно. Кроме того, известно, что справедливо и на­чальное допущение о правильности параметров подпро­граммы. Так как мы считаем, что правильность подпрограммы уже доказана, то нам не надо обращать внимание на детали строения этой программы. Мы знаем, что утверждение С5, связанное с точкой, непосредственно предшествующей опера­тору RETURN, будет справедливо и после того, как мы вернемся в основную программу. Конечно, это утверждение относится к формальным параметрам, но оно будет справед­ливо и для , фактических параметров после того, как мы вернемся и попадем в точку, с которой связано утверждение С2. Таким образом, для того чтобы убедиться в справедли­вости утверждения С2 при достижении соответствующей точки программы, следует лишь показать, что из С5' следует С2. Утверждение С5' получается из С5 заменой J1 на I, J2 на J, IQ на К и IR на L. Другими словами, из I .EQ. К * J + L AND О .LE. L AND L .LT. J следует О .LT. I AND

.LE. J AND A (I, J) AND I .EQ. K* J + L AND 0 .LE. L AND L XT. J. Читатель может легко убедиться, что из С5' не следует целиком все утверждение С2, а следует лишь под­черкнутая часть С2. Как же убедиться, что оставшаяся (невыделенная) часть также справедлива, если мы попадаем в точку, соответствующую С2? Отметим, что эта часть утверж­дения идентична утверждению С2. Следовательно, бели мы будем знать, что переменные I и J (в С1 упоминаются только они) в подпрограмме не изменяются, то можно сделать вывод, что из справедливости С1 перед обращением к под­программе следует справедливость соответствующей части С2 после обращения. Так как фактические параметры I, J сопоставляются с формальными параметрами подпрограммы Jl, J2, то теперь следует просмотреть подпрограмму: не изменяются ли значения J1 или J2. Читатель может легко проверить, что ни J1, ни J2 не изменяются. Отсюда мы делаем вывод, что утверждение О .LE. I AND 1 .LE. J AND A(I, J) продолжает оставаться справедливым и в момент достижения точки, связанной с утверждением С2.

Приведенное доказательство иллюстрирует общий метод доказательства для случаев с подпрограммами. Сначала выясняется, что делается в подпрограмме по предположению, и это доказывается обычным методом индуктивных утвержде­ний. Далее при доказательстве правильности программы, обращающейся к этой или еще и другим подпрограммам (если некоторый путь содержит такое обращение), поступаем следующим образом. Сначала доказываем, что при обращении к подпрограмме справедливо утверждение, относящееся к ее началу (здесь описываются допущения, касающиеся значений параметров). В примере мы показывали, что из С1 следует С3 Затем доказываем, что из утверждения, связанного с оператором возврата (это утверждение о правильности под­программы), следует справедливость всего (или части) утверждения, относящегося к точке (в вызывающей про­грамме), непосредственно следующей за обращением. В примере мы показали, что из С5 следует часть С2. Кроме этого, можно использовать и тот факт, что утвержде­ния, относящиеся к переменным, значения которых не изме­няются в подпрограмме, продолжают оставаться справедли­выми и после возврата из подпрограммы. В примере показано, что из С1 cледует оставшаяся часть С2 (С 1—утверждение в вызывающей программе, включающее лишь переменные, значения которых qв подпрограмме не изменились).