Ответ на »сообщение 5590« (Руслан Богатырев)
___________________________

В момент прозрения человек не думает, и это принципиально.

Это гипотеза, просто Ваша убежденность, или же Истина?

Это слова, всего лишь. Истину найдёте сами, разумеется.

Ответ на »сообщение 5591« (Geniepro)
___________________________
Ваш длинный ответ доказывает, что с базовой программистской грамотностью не все в порядке (sorry).

Но в конце вывод насчет правильных циклов -- еще одно свидетельство в пользу WHILE в этом детском споре WHILE против FOR.

Ответ на »сообщение 5593« (Руслан Богатырев)
___________________________
Или самим создавать правильные языки :)

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

Ответ на »сообщение 5591« (Geniepro)
___________________________

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

Или самим создавать правильные языки :)

Ответ на »сообщение 5588« (Миша)
___________________________
В момент прозрения человек не думает, и это принципиально.
Если интересно мнение присутствующих по этому поводу, почитайте ветку про симантическое моделирование. Там это подробно обсасывалось. Повторяться неинтересно.

Что-за такая проблема с инвариантами циклов? 8-о
Открываем любую книгу типа книги Калинина и Мацкевича "Универсальные языки программирования. Семантический подход" и рассматриваем все эти инварианты (используется Ада-подобный псевдокод):

Цикл while-do:

while B do
  S
end do;

Правило вывода инварианта для этого цикла такое:

            {P & B} S {P}
------------------------------------
{P} while B do S end do; {P & not B}

Цикл do-until:

do
  S
until B;

Переведём этот цикл в вид while-do:

S;
while not B do
  S
end do;

и получим правило вывода:

    {P} S {Q}, (Q & not B) => P
------------------------------------
{Q} while not B do S end do; {Q & B}

что для цикла do-until выглядит так:

{P} S {Q}, (Q & not B) => P
---------------------------
{P}  do S until B;  {Q & B}

Цикл do-while-do:

do
  S1
while B do
  S2
end do;

Этот цикл можно переписать так:

S1;
while B do
  S2;
  S1
end do;

Правило вывода:

        {P} S1 {Q}, {Q & B) S2 {P}
-------------------------------------------
{P} do S1 while B do S2 end do; {Q & not B}

Цикл Дейкстры

do
  B1: S1;
  B2: S2;
  . . .
  Bn: Sn
end do;

Правило вывода:

        forall i. (1<=i<=n => {P & Bi} Si {P})
------------------------------------------------------
{P} do B1: S1; B2: S2; ... Bn: Sn end do; {P & not BB}

где BB = exists i. (1<=i<=n & Bi)
    P  - инвариант цикла

Ну и, наконец, всеми обожаемый цикл for:

for X in диапазон do
  S(X)
end do;

Будем считать, что переменная X локальна для этого цикла (недоступна за пределами цикла) и не может изменяться внутри него (то есть, так, как это сделано в языке Ада). Тогда этот цикл эквивалентен следующей повледовательности:

S(x1); S(x2); ... S(xn)

где x1, x2,...,xn - множество значений указанного диапазона.

Так же этот цикл можно представить в таком виде:

if диапазон'FIRST <= диапазон'LAST then
  block
    x : диапазон'TYPE := диапазон'FIRST;
  begin
    do
      block
        use X : constant диапазон'TYPE;
      begin
        S(X)
      end block;
    while X < диапазон'LAST do
      X := диапазон'SUCC(X);
    end do;
  end block;
end if;

Здесь блоки введены для удовлетворения условиям о локальности переменной цикла и невозможности изменения её значения при выполнении тела цикла.

Правило вывода для цикла for:

{(диапазон'FIRST<=X<=диапазон'LAST) & P([диапазон'FIRST..X))}
                            S(X)
                  {P([диапазон'FIRST..X])}
-------------------------------------------------------------
            {P([диапазон'FIRST..диапазон'FIRST))}
              for X in диапазон do S(X) end do
            {P([диапазон'FIRST..диапазон'LAST))}

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

Ответ на »сообщение 5588« (Миша)
___________________________

В момент прозрения человек не думает, и это принципиально.

Это гипотеза, просто Ваша убежденность, или же Истина?

Ответ на »сообщение 5558« (Как слышно? Приём!)
___________________________

Откуда здесь дитяти, а тем более младенцы?
Миша, Вы не в курсе.
Системы не при чём.
Тут бой оберонистов с функциональщиками.

Не далее как три дня назад было тут и про "Целеустремлённые системы", и про моделирование.
Понятно, что тема - про Обероны, просто пишу по факту дискуссии.

Ответ на »сообщение 5557« (Руслан Богатырев)
___________________________

Будет время, прочитайте последний абзац моей заметки про Пойа: http://rbogatyrev.livejournal.com/

Замечательно.
Только схема, предложенная Пойа, несколько однобока, несмотря на наличие в ней "прозрения".
Мне показалось, что он относит это явление к умственной деятельности, в то время как природа его иная. В момент прозрения человек не думает, и это принципиально.
А то, что у Пойа в схеме расположено по периметру квадрата, уже - продукт логической обработки (работы ума).
Вот это перевешивание в сторону умственной деятельности, IMHO, и будет уводить от понимания того, о чём Вы поведали в последнем абзаце статьи.

Ответ на »сообщение 5584« (info21)
___________________________

Ответ на »сообщение 5582« (Денис Зайцев)
___________________________

... Или пользуйтесь WHILE или REPEAT UNTIL. ...


Что и требовалось доказать.

А переменная цикла в инварианте может оказаться помимо нашего желания.

Мне тоже в голову пришло: "Вот ведь коварный FOR!" :)
Но все-таки дело в моей небрежности: говорил о FOR, а думал о WHILE.
(Отсюда и другой ляп: мол, не знаю, как назвать это место -- началом или концом цикла. А ведь в FOR инкремент/декремент управляющей переменной вынесен из тела цикла, так что начало и конец тела цикла совсем не совпадают.)

BTW, отказ Вирта от цикла FOR в Обероне-1 сказывается-таки на деталях программирования.
На Обероне мы пишем FOR i := 0 TO LEN(a)-1 DO ... END, в то время как на Модуле-2 писали FOR i := 0 TO HIGH(a) DO ... END.