OberonCore

Если у нас нижняя граница для индексов 0, а верхняя меняется (что весьма распространенный случай), то получить список последовательных наборов индексов можно так:

где maxs -- список верхних границ индексов.
Пример получения наборов индексов для двумерного массива 5x4:

Список, как понимаете, ленивый, так что для обхода массива вполне себе годится. Считайте это не списком а итератором.

Ну и наконец общий случай, когда у нас может меняться как верхняя, так и нижняя граница:

Пример использования (двумерный массив с первым индексом от -2 до 2, вторым индексом от 2 до 4):

Можете как-то прокомментировать ход решения? Это ведь самое интересное.
Не понял этой фразы и последующего куска кода. При чем тут это?

Может кому будет интересна статья:
Regular, Shape-polymorphic, Parallel Arrays in Haskell

Ход решения весьма спонтанный. Собственно, в условии Вашей задачи и было дано почти всё решение: взять последний элемент, и добавить к нему единицу. Если переполнение, то "занулить" этот элемент и перейти к предпоследнему (здесь в силу определённых причин имеет смысл использовать цикл).

Если немного проанализировать данную схему, то видно, что если к текущему элементу прибавить единицу, и переполнения не случится, значит все элементы правее этого будут иметь минимальные значения, а элементы левее - останутся неизменными.

Выводом инварианта и ко. в явном виде не пользовался, но сейчас думаю, что они выглядит примено так.
Постусловие: переполнение или найден текущий элемент последовательности, который нужно увеличить на 1. Если текущий индекс обозначить через i, а минимально допустимое значение i = 0, то переполнение - это i < 0 (были локально переполнены все элементы последовательности)
Предусловие: имеется последовательность.
Инвариант: все элементы правее текущего имеют минимальное значение (поскольку имело место локальное переполнение).



М-да, я написал текст, а потом вставил код, в результате чего текст оказался разорванным.
Имеется в виду, что между Вашим заданием и задачей, решаемой приведённым кодом, есть разница.

Вот пароль на архив: SPwTXMtM6vIcRe1
Там лежит вот что

А мой инвариант считать правильным можно?

Вполне. У меня - "имеют правильное значение", у Вас более точно: все элементы правее текущего имеют минимальное значение (поскольку имело место локальное переполнение).