.... помогли тебе твои...
Эх, и не говорите
нет от них никаких доходов, интерес один...
Ну, в таком случае, может, хоть вы напишете "правильное постусловие". А то trurl заглох, по своему обыкновению.
Только тогда текст должен присутствовать не в форме "это надо перенести сюда", а полностью.
В конце концов, я же предупреждал, что решение должно быть "образцово-показательно".
Если я буду составлять этот цикл с нуля, с полными рассуждениями, то буду делать это так.
Итак, наш метод поиска: последовательный просмотр элементов последовательности, пока не будет обнаружена игла или не конец последовательности.
Целевое постусловие:
в последнем просмотренном сундуке обнаружена игла или нет непросмотренных сундуков
(Проверяем, что учли пограничные случаи: очевидно, что "все сундуки просмотрены и в последнем найдена игла" тоже покрыто нашим постусловием, также учитываем случай пустой последовательности сундуков - сначала я написал "все сундуки просмотрены", но заменил на более однозначное к этому случаю "нет непросмотренных сундуков").
Начнём с определения варьируемых переменных.
Заведём для последовательного просмотра переменную i, пусть она хранит номер первого ещё не просмотренного сундука.
Если бы у нас не было вложенности и был простой просмотр сундуков, то мы бы этой переменной и ограничились. Но мы понимаем, что найденную иглу надо запоминать и вводим переменную "игла", смысл которой - хранить обнаруженную иглу. А так как из нашего метода поиска вытекает, что она может быть найдена только в последнем просмотренном сундуке (а в остальных её нет), то более строго скажем: "игла" хранит результат поиска иглы в i-1-м сундуке или NIL, если i = 0.
Инвариант:
(i > 0) & (i <= len) & (игла = результату поиска иглы в i-1-м сундуке) & (в интервале [0, i-1) нет игол) OR (i = 0) & (игла = NIL)
После введения переменных и формулировки инварианта мы можем более строго сформулировать постусловие нашего поиска:
(игла # NIL) & (игла обнаружена в i-1-м сундуке) & (в интервале [0, i-1) игол не было обнаружено) OR (игла = NIL) & (в интервале [0, len) игл не было обнаружено)
Далее придумывается условие завершения цикла, которое в конъюнкции с инвариантом даст нам такое постусловие:
(игла # NIL) OR (i = len)
Отсюда сам цикл, с обратным условием продолжения:
i := 0;
WHILE (игла = NIL) & (i # len) DO
искать иглу в i-м cундуке;
INC(i)
END