Результат: ученик выбирает форму повторения по способу управления остановкой, доказывает частичную корректность и завершимость и выводит точное число операций и асимптотический класс из изменения состояния.

Содержание:

  1. Разобрать структуру цикла

    • начальное состояние;
    • условие продолжения;
    • тело итерации;
    • изменение управляющего состояния;
    • проверка условия до или после первого шага.
  2. Выбирать между for, while и do while

    • for для заранее описанного диапазона;
    • while для остановки по изменяющемуся состоянию;
    • do while при обязательной первой попытке;
    • эквивалентные преобразования между формами;
    • выбор по смыслу, а не по внешней длине кода.
  3. Управлять индексным диапазоном

    • полуинтервал [0, n);
    • первый и последний обрабатываемые элементы;
    • прямой и обратный обход;
    • пустой диапазон;
    • ошибка на единицу;
    • точное число итераций.
  4. Строить накопительное состояние

    • счётчик;
    • сумма и произведение;
    • минимум и максимум;
    • текущее и лучшее значение;
    • состояние обработанного префикса;
    • нейтральная затравка и затравка первым элементом.
  5. Организовать остановку по состоянию

    • маркер и специальное значение;
    • достижение порога;
    • первый успешный или неуспешный случай;
    • повторный запрос ввода;
    • break как досрочный выход;
    • continue как переход к следующей итерации без потери прогресса.
  6. Работать с вложенными циклами

    • независимые прямоугольные диапазоны;
    • зависимая внутренняя граница;
    • треугольное число итераций;
    • согласованные счётчики;
    • отделение внешнего состояния от внутреннего.
  7. Доказывать завершимость

    • мера прогресса;
    • ограниченность меры снизу или сверху;
    • строгое изменение на каждом продолжающем пути;
    • обнаружение состояния без прогресса;
    • предусловия, при которых доказательство действительно.
  8. Доказывать частичную корректность

    • формулировка инварианта;
    • истинность до первой итерации;
    • сохранение телом цикла;
    • связь инварианта и ложности условия с постусловием;
    • инвариант нескольких согласованных накопителей.
  9. Обрабатывать численный критерий остановки

    • содержательный допуск;
    • изменение приближения;
    • обнаружение отсутствия машинного прогресса;
    • независимый MaxIterations;
    • различие естественного завершения и достижения предела.
  10. Учитывать машинные риски цикла

    • переполнение счётчика;
    • неизменившееся дробное значение после прибавления малого шага;
    • недостижимая граница;
    • ошибка знака изменения;
    • ветвь continue, пропускающая обновление меры.
  11. Оценивать количество работы

    • размер входа n;
    • точный счётчик операций для контрольного входа;
    • последовательные фрагменты;
    • вложенные и зависимые диапазоны;
    • O(1), O(log n), O(n), O(n log n) и O(n²);
    • различие класса роста и фактического времени.