Определения элементов цикла

Рассмотрим формальные определения терминов, приведенных выше.

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

Предусловием называется состояние переменных перед выполнением цикла. Это условие должно совпадать с инвариантом, в который подставили некоторые конкретные значения переменных. Во многих случаях предусловие цикла не совпадает с данными задачи. В таких случаях нужно произвести некоторые действия (которые чаще всего заключаются в присвоении значений переменным), которые приводят к выполнению предусловия. Эти действия называются инициализацией цикла.

Постусловием называется состояние переменных после выполнения цикла. Это условие также должно совпадать с инвариантом, в который подставили некоторые конкретные значения переменных. При этом постусловие должно соответствовать условию решения задачи. В некоторых случаях нужно сделать еще несколько действий вне цикла для достижения условия решения.

Частью постусловия является условие окончания (или условие выполнения) цикла. Эта часть постусловия должна дать возможность определить, что инвариант пришел к состоянию предусловия.

Телом цикла называются действия внутри цикла. Эти действия должны, во-первых, приблизить условие окончания цикла, во-вторых, сохранить инвариант на каждом шаге. Обычно тело цикла записывается по примерно следующему алгоритму: определяется шаг цикла, который приближает предусловие, затем определяются действия, которые обеспечивают условие инварианта после шага цикла.

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