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

Функции объявляются следующим образом

function имя_функции [(список_параметров)]тип_результата;

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

[(параметры)]тип_результата; forward;

Процедуры следует объявлять так procedure имя_процедуры [(список_параметров)];

Если объявление процедуры оторвано от ее описания, нужно поставить после него ключевое слово forward

procedure имя_процедуры [(список_параметров)]; forward;

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

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

имя_подпрограммы(список_аргументов)

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

• [пусто]. Параметр передается по значению т.е. создается копия переменной основной программы.

• [var]. Параметр-переменная. Работа в подпрограмме идет напрямую с переменной основной программы.

• [const]. Неизменяемый параметр.

Глобальные объекты - это типы данных, константы и переменные, объявленные в начале программы до объявления любых подпрограмм. Эти объекты будут видны во всей программе, в том числе и во всех ее подпрограммах. Глобальные объекты существуют на протяжении всего времени работы программы.

Локальные объекты объявляются внутри какой-нибудь подпрограммы и видны только этой подпрограмме и тем подпрограммам, которые были объявлены как внутренние для нее. Локальные объекты не существуют, пока не вызвана подпрограмма, в которой они объявлены, а также после завершения ее работы. Если имеются глобальная и локальная переменные с одинаковым именем, то изнутри подпрограммы к глобальной переменной можно обратиться, приписав к ней спереди имя программы

имя_программы.имя_глобальной переменной

Процедурный тип данных. Имена подпрограмм могут выступать в роли аргументов для других подпрограмм.

Описание В разделе type процедурный тип данных задается одним из следующих способов

имя_типа = function[(список_параметров)]тип_результата;

или

имя_типа = procedure[(список_параметров)];

Например type func = function(a,binteger)integer;

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

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

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

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

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

Каждая переменная имеет тип и принадлежит к некоторому классу памяти. Время жизни и область действия идентификатора определяются ассоциированным с ним классом памяти. Существуют четыре разновидности классов памяти (С++)

auto - автоматический - локальные идентификаторы, память для которых выделяется при входе в блок, т.е. составной оператор, и освобождается при выходе из блока. Слово auto является сокращением слова automatic.

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

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

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

5. Основы доказательства правильности программ: метод мате­матической индукции, принципы простой и модифицированной индукции, доказательство правильности схем программ, метод индуктивных утверждений.

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

Принцип простой индукции:

Пусть S(N) — некоторое высказывание о целом числе N и требуется доказать, что S(N) справедливо для всех положи¬тельных чисел N.

Согласно простой математической индукции, для этого необходимо

1. Доказать, что справедливо высказывание S(1).

2. Доказать, что если для любого положительного числа N справедливо высказывание S(N), то справедливо и высказывание S(N + 1).

Принцип модифицированной простой индукции:

Иногда необходимо доказать, что высказывание S(N) справедливо для всех целых N>N0. Для этого можно довольно легко модифицировать принцип простой индукции. Чтобы доказать, что высказывание S(N) справедливо для всех целых N, необходимо:

1. Доказать, что справедливо S(N0)

2. Доказать, что если S(N) справедливо для всех целых N>N0, то справедливо и S(N+ 1).

Простая нисходящая индукция:

1. Доказать, что справедливо S (п0)

2. Доказать, что если справедливо S (п), то для любых целых n0 <=n<=M0–1 справедливо и S(N + 1).

Простая восходящая индукция:

1. Доказать, что справедливо S(M0).

2. Доказать, что если справедливо S(N), то для любых целых n0+1<=n<=M0 справедливо и S(N – 1).

Основные принципы доказательства правильности для блок-схем:

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

1. Доказать, что справедливо S(1), т. е. справедливо высказывание S при первом проходе через точку.

2. Доказать, что если справедливо S(N) (т. е. при N-ом проходе через точ-ку), то справедливо и S(N+1), если мы, конечно, попадем в точку в п+1-й раз.

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

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

Попробуем доказать это методом индукции по N – числу проходов через точку 2.

1. При первом попадании (N = 1) в точку 2 (сюда мы приходим из точки 7) имеем I = 0 и J=0. Утверждение J = I*N = 0*N = 0, таким образом, справедливо.

2. Предположим, что J = I*N справедливо при N-ом попадании в точку 2. Нужно показать, что если мы попадем в точку 2 в N+1-й раз, то утверждение J=I*N опять будет справедливо. Пусть I и J при N-ом проходе через точку 2 принимают значения IN и JN. Тогда гипотеза индукции есть JN=IN*N. Единственный способ вновь попасть в точку 2 – выполнить тело цикла (точнее, пройти «по петле»), пройдя через точки 3, 4 и возвратясь опять в точку 2. Если это именно так, то, однажды проследив выполнение тела цикла, мы видим, что при возвращении в точку 2 новое значение I равно предыдущему значению плюс 1, а новое значение J – предыдущему значению плюс N.

Следовательно, если мы вновь попадем в точку 2 в п N+1-й раз, то J = I*N. Доказательство по индукции на этом заканчивается, и мы видим, что при любом попадании в точку 2 справедливо утверждение J = I • N.

Докажем с помощью восходящей индукции по M – переменной, удовлетворяющей условию 0<=M<=M, – что мы когда-нибудь достигнем точки 2 с I=M (т.е. программа закончится).

1. При первом попадании в точку 2 имеем I=0, т. е. утверждение справедливо для M=0. Если M=0, то это уже обеспечивает конечный результат.

2. В противном случае предположим, что мы, в конце концов, попали в точку 2 и I=M при 0<=M<=M. Требуется показать, что мы попадем в точку 2 и с I=M+1. В точке 2 с I=M и 0<=M<=M отношение I = M ложно, так как M < M, и, следовательно, мы пройдем по циклу и вернемся в точку 2. При таком возврате значение I увеличится на 1, т. е. очевидно, что мы попадем в точку 2 со значением I = M + 1, что и требовалось доказать.

Метоод индуктивных утверждений.

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

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

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

Определение 2. Будем называть программу (блок-схему) полностью правильной (по отношению к А и С), если она частично правильна (по отно-шению к А и С) и заканчивается при всех данных, удовлетворяющих А.

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

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

Сокращенные доказательства правильности

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