Информационный сайт

 

Реклама
bulletinsite.net -> Книги на сайте -> Программисту -> Непейвода Н.Н. -> "Основания программирования " -> 117

Основания программирования - Непейвода Н.Н.

Непейвода Н.Н., Скопин И.Н. Основания программирования — Институт компьютерных исследований , 2002. — 919 c.
Скачать (прямая ссылка): osnovanprogramm2002.pdf
Предыдущая << 1 .. 111 112 113 114 115 116 < 117 > 118 119 120 121 122 123 .. 316 >> Следующая

12 Недоведенность до конца принципиально новых возможностей, ощущавшихся создателями Алгола-68, явилась основной бедой данного языка.
7.3. ЛОГИЧЕСКАЯ СТРУКТУРА ЦИКЛА
331
для любого потокового цикла является ординал, задающий верхнюю оценку числа оставшихся шагов. Поскольку любая убывающая последовательность ординалов за конечное число шагов доходит до нуля, то наличие такого призрака гарантирует конечность цикла.
роблема параметров цикла тесно связана с другой проблемой. акова логическая сущность цикла, задающего потоковую обработку?
Потоковый цикл соответствует математическому доказательству по индукции. Базис индукции — его инициализация, шаг индукции — итерация цикла, а заверение соответствует переходу от индуктивного утвердения к тому, что требовалось доказать.13
Теперь рассмотрим форму рассуждения по индукции. Шаг индукции имеет вид (мы выписали его с явным указанием всех параметров цикла):
Здесь видно, что при индукции изменяются значения параметров, но сохраняется отношение между ними. В математике это отношение называется предположением (или утвеждением) индукции, в программировании — инвариантом цикла.
Пример 7.3.1. Для программы Prime_Numbers_1 инвариантом основного цикла является простая логическая формула
где Prime — предикат 'Быть простым числом'. Для следующей программы Prime_Numbers_2 инвариант основного цикла формулируется значительно сложнее. Его удобнее записать в виде предложения русского математического языка:
Pr(j) i < Pr(J + 1), где Pr — функция, перечисляющая простые числа в порядке возрастания, и Prime имеет значение Pr(j) = i, и для всех k < j a[k — 1] = Pr (к).
13 Даже проблема призраков впервые была осознана в математической логике именно для рассуждений по индукции — парадокс изобретателя: очень часто для успешного доказательства по индукции требуется усилить доказываемое утверждение, а в дальнейшем было строго обосновано, что имеются утверждения вида
где / — вычислимая функция, для доказательства которых нужно привлекать сущности сколь угодно высоких порядков (см., напр., [63]).
(7.1)
Prime <=>¦ Prime(i)
Vi/ (i)=0,
332
7.
ля последуих вариаций программ инвариант цикла ее болье усло -няется.
Заметим, что в инвариантах часто используются теоретические предикат и теоретические функции, в некотором смсле дублируие вчисляе-мые в программе значения (например, a [к — 1] и Pr (к) вше). Это необходимо, поскольку, задавая призраки, м отвлекаемся от вопроса об их вчи-слимости и концентрируемся на их свойствах и их отношениях к понятиям программы. Эти понятия, в частности, могут в отдельных случаях и совпадать с призраками (ведь функция Pr (к) определена для всех натуральных к, а не только для мно ества индексов массива). Конец примера 7.3.1.
Предикат, принимающий значения истина, пока выполняется тело цикла, и ложь, когда выполнение тела цикла прекращается, называется полным инвариантом цикла. Для выделенного ниже, в программе 7.3.2, цикла имеется, например, следуий полнй инвариант:
(imi <= ima) && (x != a[( imi + ima )/2 ]) олнй инвариант суественно зависит от выбора присутствуих в нем значений и призраков и, да е если их вбор фиксирован, мо ет бть не единственным.
7.3.2. Цикл Дейкстры и цикл-'паук'
анный параграф перебрасывает мостик к следуей теме наего изло-ения: циклам, не являимся потоковыми. Э. ейкстра, осознав концеп-ци охраняемых команд, не мог не перенести ее и на конструкции цикла. В оригинальной форме цикл Дейкстры имеет вид
do
Pi — Si,
Pn — Sn,
od
терация, как и в условном операторе с охраняемыми командами, начинается с совместного вычисления охран. Затем выбирается то из действий, которое соответствует истинной охране (если истинных охран несколько, то, как и в условном операторе, лбое, но одно). Вполняется это действие, и цикл возобновляется.
7.3.
333
Таким образом, условие выхода из цикла неявно: это ложность всех охран. Заметим, что Дейкстра противоречит сам себе в определении цикла и условного оператора. В условном операторе он резко выступал против умолчаний и на этом основании отвергал часть else. В операторе цикла он же суще-ственнейим образом использовал умолчание как критерий заверения цикла. Если уж явно выписывать условия, то все существенные .Альтернатива возможна лишь для вылавливания непредусмотренных случаев, возможно, вызванных неправильным использованием программы. Поэтому предлагается следующий вариант цикла (цикл-'паук'), в котором условия завершения так е перечислены явно и есть альтернативное заверение else, например, для сообения об оибке.
do
Pi — Si ,
Pn — Sn,
out
Q1 — T1,
Qm — Tm,
else
Error_Analysis
od
В отличие от традиционного цикла, логические корни цикла Дейкстры и цикла-паука находятся в таких логиках, которые противоречат классической, например, в нильпотентных логиках. Эти формы циклов естественно сопря-га тся с программированием от состояний, а при структурном программировании они нужны лишь для действий, которые трудно сводятся к потокам. 7.3.3. Совместный цикл
Какую дисциплину выполнения цикла не отражает ни цикл for, ни другие виды циклов в языке С ив других языках традиционного типа? Нет цикла, итерации которого выполнялись бы независимо от того, в каком порядке появляются значения параметра цикла .Иными словами, хотелось бы иметь в языке конструкци
Предыдущая << 1 .. 111 112 113 114 115 116 < 117 > 118 119 120 121 122 123 .. 316 >> Следующая
Реклама
Авторские права © 2009 AdsNet. Все права защищены.
Rambler's Top100