Вопрос 28

3. Корректность программы

Представление о правильности программы принято формулировать в виде понятия

корректности программы, означающего, что программа должна соответствовать

спецификации. Это общее требование о соответствии программы ее спецификации

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

Допустим, программа представлена оператором S(x: y), где x и y

непересекающиеся наборы переменных. Для программы определена логика L(S(x: y)).

Спецификация программы S(x: y) задается двумя предикатами: предусловием P(x),

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

постусловием Q(x, y), связывающим значения аргументов и результатов. Спецификация

изображается следующим образом: [P(x), Q(x, y)]. Программа S(x: y) со спецификацией

записывается в виде известной тройки Хоара {P(x)} S(x: y) {Q(x, y)}, см. [2].

Пусть точка 1 определяет начало исполнения программы, а точка 2 – конец

исполнения. Корректность программы определяется следующими двумя условиями:

предусловие P(x) должно быть истинным в точке 1;

постусловие Q(x, y) должно быть истинным в точке 2.

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

исполнение программы. Однако допустимо ли, чтобы исполнение не завершалась? Нет.

Бесконечное исполнение бессмысленно, поскольку в соответствии с исходным

предположением программа не взаимодействует с окружением. Поэтому необходимо

третье условие корректности:

исполнение программы всегда завершается.

Истинность предусловия P(x) невозможно проверить статически для программы

S(x: y). Возможна лишь динамическая проверка предусловия перед началом исполнения

программы. Однако статическая проверка предусловия может быть проведена для вызова

программы S из другой программы.

Предусловие P(x), истинное в точке 1, будет также истинным и в точке 2,

поскольку программа S(x: y) не меняет значений набора переменных x. Поэтому

истинность второго и третьего условий корректности, ассоциированных с точкой 2,

достаточно доказать при условии, что P(x) истинно.

Предикат L(S(x: y)) становится второй посылкой при доказательстве второго

условия корректности, поскольку в точке 2 истинно L(S(x: y)). В соответствии с

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

предикатом y. L(S(x: y)). В итоге второе и третье условия корректности принимают

следующий вид:

P(x) & L(S(x: y)) Q(x, y) (9)

P(x) y. L(S(x: y)) (10)

Формула (9) называется условием частичной корректности, а (10) условием

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

корректности программы:

Corr(S(x: y), P(x), Q(x, y)) P(x) [ L(S(x: y)) Q(x, y) ] & y. L(S(x: y)) (11)

Далее термин «корректность» будем использовать в смысле тотальной корректности.

Вопрос 29

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

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

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

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

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

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

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

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

dd:=dd/2;

if ddr do r:=r-dd

сохраняет отношения

0<=r<dd

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

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

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

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

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

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

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

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

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

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

Из сказанного можно сделать следующий вывод. Если мы считаем своей обязанностью контролировать вычисления (интеллектуально!), обращаясь к тексту управляющей вычислениями программы, то нам следует смиренно довольствоваться наиболее систематизированными способами организации следования, гарантирующими самое непосредственное отражение "продвижения вычислений" в "продвижении по тексту".