Насколько я понимаю, под выражением смысла цикла Вы понимаете явное и формальное оперирование предикатами.
Мне представляется, что это предрассудок (если только мы не занимаемся теорией доказательств).
Не обязательно. Формальность должна быть ровно в той мере, в какой она проясняет понимание. Доказательство - это представление в такой форме, в которой правильность очевидна, а не нагромождение формул ради формул.
Касательно примера Евгения Темиргалеева - я уже не помню деталей, но суть в том, что комбинаторный перебор в той задаче был неэффективен. Надо было найти соотношение между цифрами числа, выбрать первое такое число - а затем проработать шаг к следующему числу (с восстановлением инварианта). Вместо 1000 итераций получалось несколько десятков.
И тут, конечно, Вы меня начинаете критиковать за "нестрогость" и несоответствие образцу линейного поиска.
Как человек малограмотный, я пропускаю мимо ушей замечание о несоответствии образцу, но критика "нестрогости" задевает меня за живое.
"Где же здесь нестрогость?" - спрашиваю я в ответ. - "Напротив, всё очень строго. Как я рассуждаю? Если я нашёл элемент с нужным именем, то моя задача выполнена, и я сразу возвращаю требуемое значение.
Вообще меня всегда поражали эти споры касательно метода Дейкстры.
Вот в третьем классе детям на математике начинают объяснять, что такое уравнения (по крайней мере по занковской системе мы их тогда уже активно изучали). И с их помощью начинают решать задачки. Те же самые, которые раньше решались по действиям с задействованием "общей соображалки". И ведь точно так же было непонятно "а на хрена ж эти уравнения сдались, мы вот и под действиям сообразим"... Только задачи бывают и на порядок сложнее, а при владении единым методом щёлкаются как семечки. Есть общий мат. метод составления уравнений. А есть "партизанские вилы".
Как-то в переписке с Алексеем Донским мы беседовали на эту тему. Уже тогда я попросил разрешения опубликовать, повода не было.
Alexey_Donskoy писал(а):
Увы мне - фундаментальность и необходимость математического обоснования алгоритмических решений потерпела ещё одно поражение в моём сознании
Её просто не нужно абсолютизировать, считать панацеей и использовать не к месту... Вообще же иметь это знание в своём багаже весьма полезно.
Я в чистом виде к математике больших склонностей не имею, поэтому предпочитаю всегда полуформальный путь. Ровно настолько, чтобы было что-то очевидно или ощущаемо... Верификация, с моей точки зрения, - это представление проверяемого объекта в такой форме, в которой его правильность очевидна. И мат. формализмы здесь нужно применять ровно столько и так, чтобы они содействовали этому принципу.
Так вот, расскажу, как я понимаю суть "математического обоснования алгоритмических решений". Соль метода Дейкстры, в общем. Буду стараться очень простыми словами, с прицелом на то, чтобы текст потом "повторно использовать"
Если ты не против, то это я бы вынес на форум.
Состояние программы в каждый момент времени, если программа выполняется правильно, в некотором смысле целостно ("всё идёт, как надо"). А "как надо"? Это так, что об этом состоянии можно сделать какие-то логические утверждения (предикаты от переменных), которые будут истинны. Посему Хорошая Мысль в истории грамотного программирования - формулировать о состоянии программы в разных местах. логические утверждения.
Самое главное, что вообще, на мой взгляд, нужно всегда и везде - это понятие пред- и постусловий. Любая система строится блочно-модульно (Римский принцип "разделяй и властвуй"). Даже небольшой алгоритм состоит обычно из нескольких частей, которые передают друг другу управление (в простейшем случае - по очереди). Как проверить, что части взаимодействуют правильно? Явно обдумать и записать правила этого взаимодействия (формализовать - полностью или частично).
Пред- и постусловия как раз позволяют составить договор между взаимодействующими частями - контракт. Блок имеет требуемое предусловие (то, что должен обеспечить клиент) и гарантируемое постусловие (которое блок обеспечивает, если клиент соблюл предусловие). В точке же использования блока можно сформулировать гарантируемое предусловие (в линейном коде это постусловие предшествующего блока) и требуемое постусловие (что нужно). Контракт считается обеспеченным, если гарантируемое предусловие эквивалентно либо сильнее (имплицирует) требуемое предусловие, и требуемое постусловие эквивалентно либо слабее (следует) гарантируемого постусловия.
Практика показывает, что для процедур и более крупных частей явно формулировать (можно полуформально, с обычными словами) пред- и постусловия стоит всегда. Кроме того, предусловия нужно ещё и явно проверять неотключаемым ASSERT-ом - это в разы облегчает по времени и трудоёмкости поиск некоторых ошибок. Исключения в этих правилах можно делать только для небольших внутренних процедур модуля.
Теперь идём дальше, к понятию инварианта. В общем смысле оно, понятно, что означает. И в этом общем смысле оно тоже ценно, как раз в связи с контрактным программированием. Любой компонент должен давать какие-то гарантии относительно процесса своей работы. Если он без побочных эффектов (просто функция), то говорить об инварианте смысла вообще нет. А вот если побочные эффекты предусмотрены, то важно знать, каких эффектов гарантированно не будет, т.е. инварианты контракта с этим компонентном. Мы применительно к Оберону любим говорить об инвариантах — в том смысле, что при программировании на нём гарантируется незыблемость каких-то условий. Самое главное — инварианты памяти, гарантии относительно того, что указатель либо указывает на существующий объект, либо NIL. Не менее важен инвариант о том, что нельзя средствами языка, не включая средства псевдомодуля SYSTEM, получить и запомнить адрес VAR-переменной. Это позволяет строить библиотечные средства, которые гарантируют более сложные инварианты. (Например, некоторый описатель объекта, который даёт доступ к его состоянию только в определённое время, указанной процедуре-обработчику и т.п.)
Ну и наконец об инварианте цикла. Я вообще не очень люблю этот термин, он как-то не раскрывает существа дела. Тут скорее не просто инвариант, а главное соотношение цикла.
Суть можно передать фразой, которую очень любит Паронджанов: «трамвай ходит только по рельсам». Так и цикл — любой имеющий смысл цикл идёт по каким-то рельсам, и только по ним. Инициализация цикла — это его постановка на рельсы, затем происходит движение, потом — остановка, но тоже ещё на рельсах. Вот инвариант цикла — это и есть те рельсы, по которым он идёт. Обычно пишут: логическое условие, которое истинно в начале цикла и после каждой его итерации (в том числе по окончании) — это само по себе ничего не объясняет, конечно. Можно найти огромное количество инвариантов к циклу, которые не имеют смысла — ясно, что любое условие относительно неизменяемых в цикле переменных, будучи истинным в начале, останется таковым и в конце. Соль в том, чтобы указать то соотношение, которым связаны переменные, изменяемые в цикле. Тогда на каждом витке цикла мы продвигаемся по рельсам вперёд — восстанавливаем это соотношение для очередного отрезка нашего пути решения задачи.
Пример с копированием из массива в массив как раз вполне удачен для иллюстрации инварианта. Ставим задачу: скопировать массив. Иначе говоря, сделать все элементы соответственно равными (ясно, что можно записать логич. условие с квантором всеобщности по индексу). Ищем путь решения. Нас осеняет: можно же копировать элементы один за другим. А в каком порядке? Давайте слева направо. Будет цикл. А как будут выглядеть массивы на каждом шаге цикла? Некоторый левый кусок у них будет одинаковый, а остальную часть ещё надо копировать. Обозначим за i правую границу (не включающую) того отрезка массива, который уже скопирован. Тогда «рельсы цикла», инвариант:
A j: 0 <= j < i : Dest[j] = Src[i] (где A — это квантор всеобщности, «для любого»). Будем двигаться по рельсам вперёд — т.е. увеличивать в цикле i. Чтобы восстанавливать инвариант, будем копировать очередной элемент. Условием окончания поставим, очевидно, i = n. Проверяем: после окончания цикла для A j: 0 <= j < i = n : Dest[j] = Src[i], что нам и требовалось. А чаще инвариант как раз из постусловия и получают — т.е. ослабляют постусловие так, чтобы его можно было сделать истинным уже до цикла, а потом в цикле постепенно прилижать к цели (метод «сдувания воздушного шарика»). Как раз если в нашем случае постусловии сделать правую границу плавающей, то тут и получаем инвариант... Ясно, что для нашего простого случая всё это подробно раскручивать смысла нет. Но понятие инварианта ценно всегда. Сказать инвариант — значит, сказать смысл цикла — и наоборот. «Копируем массив поэлементно слева направо» - вот инвариант. С соотв. записью в логич. условиях с кванторами.
Рассмотрите, например, простую сортировку прямым выбором. Формулируем суть: будем собирать отсортированную последовательность начиная с минимальных элементов, т.е. на каждом шаге брать из оставшихся элементов минимальный и добавлять его в отсортированный список. «Детское решение» - перенося элементы в другой массив. «Взрослое» - обойтись тем же массивом. Будем переставлять элементы так, чтобы с левого края собиралась отсортированная последовательность. На каждом шаге будем добавлять к последовательности по одному элементу. Тогда как у нас выглядят данные на каждом шаге?
Есть некоторое i, слева от которого расположена отсортированная последовательность, а справа — оставшиеся элементы, каждый из которых больше или равны, чем любой из отсортированных. То есть, инвариант: отосортировано(0, i) И ( A j, k: (0 <= j < i) И (i <= k < n) : m[j] <= m[k] ). Тогда «вперёд по рельсам» — это сдвинуть i и подобрать из оставшихся такой элемент, чтобы была верна вторая часть инварианта — т.е. минимальный из них. Можно записать цикл, обозначив поиск этого элемента пока просто псевдооператором «найти..». Проверям, что в конце цикла приходим к требуемому постусловию отсортировано (0, n) (а могли бы идти от него через ослабление). Мы не разворачивали условие для «отсортировано» - это нам не нужно Мы просто идём от рекурсивного определения: отсортировано(0, i) <=> ИСТИНА, если i = 0, и <=> отсортировано(0, i-1) и (i-й элемент больше или равен всех предыдущих). Мы выбрали такой инвариант, что это условие соблюдается. Это пример того, что расписывать громадные условия не нужно, нас совершенно здесь не интересует, как там проверить свойство отсортированности через кванторы, мы просто понимаем его конструктивно (если к отсортированной последовательности добавить элемент, больших всех её элементов, то она останется отсортированной). Ну, точно так же проектируем внутренний цикл поиска минимального элемента — пошаговая детализация с уточнением (сначала внешний цикл, обозначив внутренний только псевдокодом «найти», потом начинаем разворачивать этот псевдокод).
Да, и здесь на практике мы не будем так подробно всё раскручивать и расписывать, но разве подобные рассуждения не соответствуют естественному внутреннему ходу мысли? А инвариант опять прост и полезен: «левая часть массива отсортирована, правая содержит оставшиеся элементы, превосходящие отсортированные». Его даже и записать комментарием к циклу будет полезно, свернув до логич. условия, т.к. цикл уже не самый простой, а с вложенным.
В общем, надеюсь, проиллюстрировал пользу инварианта и вообще основательного подхода к алгоритмике...