OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 19 Апрель, 2019 09:50

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 165 ]  На страницу Пред.  1, 2, 3, 4, 5, 6 ... 9  След.
Автор Сообщение
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Воскресенье, 16 Ноябрь, 2008 23:40 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8047
Откуда: Троицк, Москва
[quote="Илья Ермаков]Инвариант не для борьбы с goto придуман, а для[/quote]корректного построения циклов.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Воскресенье, 16 Ноябрь, 2008 23:54 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9115
Откуда: Россия, Орёл
Да, конечно.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 01:20 
Аватара пользователя

Зарегистрирован: Суббота, 19 Ноябрь, 2005 15:59
Сообщения: 803
Откуда: Зеленоград
Илья Ермаков писал(а):
Я имел в виду, что для того, чтобы написать цикл, нужно сначала выразить строго его смысл. Что и делается с помощью инварианта.
Ваша мысль понятна.
Однако, неочевидна мера "строгости", необходимой для построения циклов.
IMHO, эта мера не так бесспорна даже в математике (по крайней мере, ещё в XX веке случались расхождения во взглядах на доказательство).
Кроме того, существуют и практические ограничения. Например:
http://ru.wikipedia.org/wiki/Математическое_доказательство
Цитата:
Формальными доказательствами занимается специальная ветвь математики — теория доказательств. Сами формальные доказательства математики почти никогда не используют, поскольку для человеческого восприятия они очень сложны и часто занимают очень много места.
Насколько я понимаю, под выражением смысла цикла Вы понимаете явное и формальное оперирование предикатами.
Мне представляется, что это предрассудок (если только мы не занимаемся теорией доказательств).
Рассмотрим какой-нибудь пример.
Допустим, мне надо написать на Си функцию поиска в таблице с прототипом
Код:
struct def *search(const char *name);
Допустим, таблица представлена линейным списком, а я неграмотный программёр.
Итак, я начинаю "творить". :)
Что мне первое приходит в голову? Конечно, наш любимый пример с for/while и break/return.
Код:
struct def *search(const char *name)
{
    struct def *p;

    for (p = root; p != NULL; p = p->next)
        if (strcmp(name, p->name) == 0)
            return p;
    return NULL;
}
И тут, конечно, Вы меня начинаете критиковать за "нестрогость" и несоответствие образцу линейного поиска.
Как человек малограмотный, я пропускаю мимо ушей замечание о несоответствии образцу, но критика "нестрогости" задевает меня за живое.
"Где же здесь нестрогость?" - спрашиваю я в ответ. - "Напротив, всё очень строго. Как я рассуждаю? Если я нашёл элемент с нужным именем, то моя задача выполнена, и я сразу возвращаю требуемое значение. Если, перебрав все записи в таблице, я его не нашёл, то возвращаю NULL, как знак того, что элемента нет. Да, я не прибегаю к формализму, но ошибки в моём рассуждении нет."


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 01:32 

Зарегистрирован: Воскресенье, 28 Май, 2006 22:12
Сообщения: 1343
AVC писал(а):
Как я рассуждаю?

Нормально и правильно вы рассуждаете.
И - не заморачивайтесь! А то ещё комплексы наживёте... а там - и до язвы недалёко... :twisted:
Нежданный выход с return-ом - сам по себе уже (как исключение), обращает на себя внимание. и заставляет логику напрягать. Соответственно, "нетиповое" использование (не по дисциплине!) уже говорит о том, что здесь акцент на неординарном событии в алгоритме.
Впрочем, я при поиске настолько часто подобную конструкцию пользую, что уже и не гадал, что кто-то на это внимание акцентирует...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 02:02 
Модератор
Аватара пользователя

Зарегистрирован: Среда, 16 Ноябрь, 2005 00:53
Сообщения: 4488
Откуда: Россия, Орёл
AVC писал(а):
... а я неграмотный программёр. Итак, я начинаю "творить". :)
Всё верно, но
1) Это примитивный пример. Грамотный программер не начинает творить, а использует известную схему линейного поиска. В которой без рассуждений нет ошибок.
2) Для сложного цикла такие "творения" либо приведут к неэффективному решению, либо вообще непойми к чему. И то и другое в итоге будет доводиться "до ума" тыканьем в отладчике. И в итоге совершенно не очевидно, что
AVC писал(а):
ошибки в моём рассуждении нет."


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 02:11 
Модератор
Аватара пользователя

Зарегистрирован: Среда, 16 Ноябрь, 2005 00:53
Сообщения: 4488
Откуда: Россия, Орёл
Пример (рассказывал Илья Ермаков, надеюсь он уточнит условие и покажет решение с инвариантом)

Задача: найти трехзначное число, цифры которого удовлетворяют определенному условию. Один студент начал "безошибочные рассуждения" и решил вроде:
Код:
FOR i := 1 TO 9 DO
  FOR j := 0 TO 9 DO
    FOR k := 0 TO 9 DO
      IF Усл(i, j, k) THEN RETURN 100 * i + 10 * j + k END
    END
  END
END


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 03:32 
Аватара пользователя

Зарегистрирован: Суббота, 19 Ноябрь, 2005 15:59
Сообщения: 803
Откуда: Зеленоград
Давайте подумаем.
Что для нас действительно важно? Принцип "разделяй и властвуй".
Как он поддерживается в Обероне? Блочная структура, модульность, герметичность системы типов. В этом же ряду - и устранение неограниченной "свободы" goto.
Всё это действительно хорошо.
Но в пылу борьбы с goto ставятся под сомнение, а то и вовсе не включаются в язык такие конструкции как выход из середины цикла/процедуры и исключения (в смысле их языковой поддержки). Результат - неестественность кода, куда можно отнести дополнительные переменные-флаги и дублирование кода.
Что же касается исключений, то складывается впечатление, что даже нет понимания практической необходимости такого механизма. И это в языке, насыщенном исключениями: нарушение ASSERT, разыменование нулевого указателя, обращение по индексу за пределами массива, некорректное приведение к расширенному типу (type guard), иногда - переполнение, деление на нуль и т.п.
Что случится с моей встроенной программой на Обероне, если возникнет хотя бы одна из этих ситуаций? Это же не ОС Оберон, где исключения перехватываются операционкой, а потом пользователь сам вызовет следующую команду.
Предполагаю, что дело здесь в ошибочном (IMHO) отнесении программирования к ведомству математики.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 09:42 
Модератор
Аватара пользователя

Зарегистрирован: Среда, 16 Ноябрь, 2005 00:53
Сообщения: 4488
Откуда: Россия, Орёл
Алексей, речь шла о необходимости инварианта при построении цикла. И о том, что для стандартных схем этот инвариант выведен, надо только пользоваться. А для не стандартных придумывание инварианта гарантирует корректность решения и, скорее всего, его простоту (в сравнении с "творением" "от балды").

А для исключений у нас другая ветка. :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 10:39 
Аватара пользователя

Зарегистрирован: Суббота, 29 Март, 2008 19:27
Сообщения: 1031
Откуда: Россия, Чебоксары
Евгений Темиргалеев писал(а):
Задача: найти трехзначное число, цифры которого удовлетворяют определенному условию. Один студент начал "безошибочные рассуждения" и решил вроде
Что-то я не понимаю, что-ли? Вроде бы кристально ясное решение, без всяких подводных камней... Имхо, любое другое решение существенно осложнит понимание...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 10:44 

Зарегистрирован: Понедельник, 29 Январь, 2007 19:00
Сообщения: 370
Откуда: Украина, Запорожье
Евгений Темиргалеев писал(а):
Пример (рассказывал Илья Ермаков, надеюсь он уточнит условие и покажет решение с инвариантом)

Задача: найти трехзначное число, цифры которого удовлетворяют определенному условию. Один студент начал "безошибочные рассуждения" и решил вроде:
Код:
FOR i := 1 TO 9 DO
  FOR j := 0 TO 9 DO
    FOR k := 0 TO 9 DO
      IF Усл(i, j, k) THEN RETURN 100 * i + 10 * j + k END
    END
  END
END

И что здесь не так? В конце забыли поставить RETURN?
Всё-таки это тоже примитивный пример, который при желании можно свести к схеме линейного поиска:
Код:
FOR n := 100 TO 999 DO
  IF Усл(n DIV 100 MOD 10,
         n DIV 10  MOD 10,
         n DIV 1   MOD 10) THEN RETURN n END
END;
RETURN -1;

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 12:04 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9115
Откуда: Россия, Орёл
Вечером обстоятельно отвечу.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 14:04 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8047
Откуда: Троицк, Москва
Илья Ермаков писал(а):
Да, конечно.

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


(Интересно: я Вам возражаю, Вы говорите "Да,конечно", и тут же повторяете своё первое утверждение.)

Хорошо. Тогда что такое смысл цикла.
В моем понимании -- это какую задачу решает цикл.
Инвариант же определяет способ решения задачи.
В Вашем понимании смысл цикла -- это способ.
Ну, будем знать.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 17:24 

Зарегистрирован: Суббота, 26 Ноябрь, 2005 18:38
Сообщения: 1857
Илья Ермаков писал(а):
Может смотреться непривычно.


Смотрится как continue внутри for/while, усугубленный ручной игрой с переменными цикла. В сад.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 18:03 

Зарегистрирован: Понедельник, 29 Январь, 2007 19:00
Сообщения: 370
Откуда: Украина, Запорожье
Vlad писал(а):
Илья Ермаков писал(а):
Может смотреться непривычно.
Смотрится как continue внутри for/while, усугубленный ручной игрой с переменными цикла. В сад.
Это после перевода на Оберон ;), а в оригинале (у Гриса), по-моему, выглядит симметричнее и понятнее
Код:
i,j:=0,0;
do   i≠m and j≠n cand b[i,j]≠x -> j:=j+1
[]   i≠m and j=n -> i,j:=i+1,0
od


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 18:16 

Зарегистрирован: Суббота, 26 Ноябрь, 2005 18:38
Сообщения: 1857
PGR писал(а):
после перевода на Оберон ;), а в оригинале (у Гриса), по-моему, выглядит симметричнее и понятнее


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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 19:50 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 8047
Откуда: Троицк, Москва
Vlad писал(а):
Покажите реальный пример, где цикл Д. нагляднее.

Докажите, что вы прочли книжки Дейкстры и Гриса.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 20:09 

Зарегистрирован: Суббота, 26 Ноябрь, 2005 18:38
Сообщения: 1857
Info21 писал(а):
Vlad писал(а):
Покажите реальный пример, где цикл Д. нагляднее.

Докажите, что вы прочли книжки Дейкстры и Гриса.


Как? Подписаться под тем, что цикл Д. имеет смысл в современном ЯВУ? :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 20:41 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9115
Откуда: Россия, Орёл
Vlad писал(а):
Не, все равно, сути происходящего (итерация по i, j с проверкой условия) нифига не видно.

Суть происходящего - линейный поиск в линейной (!!) же последовательности, в которой переходы к следующему элементу неоднородны (иногда требуются особые действия).
Представьте себе вместо примера с двумерным массивом поиск в страничной структуре вида
Page = POINTER TO RECORD data: ARRAY 2048 OF Elem; next: Page END.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 20:46 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9115
Откуда: Россия, Орёл
Info21 писал(а):
Илья Ермаков писал(а):
Да, конечно.

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


(Интересно: я Вам возражаю, Вы говорите "Да,конечно", и тут же повторяете своё первое утверждение.)

Хорошо. Тогда что такое смысл цикла.
В моем понимании -- это какую задачу решает цикл.
Инвариант же определяет способ решения задачи.
В Вашем понимании смысл цикла -- это способ.
Ну, будем знать.


Я подумал, что изначальное моё высказывание имело интерпретацию "инвариант нужен, чтобы описать смысл постфактум" и подчеркнул, что имею в виду именно выражение перед построением.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Цикл Дейкстры
СообщениеДобавлено: Понедельник, 17 Ноябрь, 2008 21:03 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9115
Откуда: Россия, Орёл
Цитата:
Насколько я понимаю, под выражением смысла цикла Вы понимаете явное и формальное оперирование предикатами.
Мне представляется, что это предрассудок (если только мы не занимаемся теорией доказательств).

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

Касательно примера Евгения Темиргалеева - я уже не помню деталей, но суть в том, что комбинаторный перебор в той задаче был неэффективен. Надо было найти соотношение между цифрами числа, выбрать первое такое число - а затем проработать шаг к следующему числу (с восстановлением инварианта). Вместо 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-й элемент больше или равен всех предыдущих). Мы выбрали такой инвариант, что это условие соблюдается. Это пример того, что расписывать громадные условия не нужно, нас совершенно здесь не интересует, как там проверить свойство отсортированности через кванторы, мы просто понимаем его конструктивно (если к отсортированной последовательности добавить элемент, больших всех её элементов, то она останется отсортированной). Ну, точно так же проектируем внутренний цикл поиска минимального элемента — пошаговая детализация с уточнением (сначала внешний цикл, обозначив внутренний только псевдокодом «найти», потом начинаем разворачивать этот псевдокод).

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

В общем, надеюсь, проиллюстрировал пользу инварианта и вообще основательного подхода к алгоритмике...


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 165 ]  На страницу Пред.  1, 2, 3, 4, 5, 6 ... 9  След.

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


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

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2019, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB