Рассмотрим формальные определения терминов, приведенных выше.
Инвариантом называется условие, которое выполняется на каждом шаге цикла, включая значение переменных до начала выполнения цикла и после выполнения цикла. Это условие может быть записано в виде математического отношения, связывающего между собой переменные, участвующие в цикле.
Предусловием называется состояние переменных перед выполнением цикла. Это условие должно совпадать с инвариантом, в который подставили некоторые конкретные значения переменных. Во многих случаях предусловие цикла не совпадает с данными задачи. В таких случаях нужно произвести некоторые действия (которые чаще всего заключаются в присвоении значений переменным), которые приводят к выполнению предусловия. Эти действия называются инициализацией цикла.
Постусловием называется состояние переменных после выполнения цикла. Это условие также должно совпадать с инвариантом, в который подставили некоторые конкретные значения переменных. При этом постусловие должно соответствовать условию решения задачи. В некоторых случаях нужно сделать еще несколько действий вне цикла для достижения условия решения.
|
|
Частью постусловия является условие окончания (или условие выполнения) цикла. Эта часть постусловия должна дать возможность определить, что инвариант пришел к состоянию предусловия.
Телом цикла называются действия внутри цикла. Эти действия должны, во-первых, приблизить условие окончания цикла, во-вторых, сохранить инвариант на каждом шаге. Обычно тело цикла записывается по примерно следующему алгоритму: определяется шаг цикла, который приближает предусловие, затем определяются действия, которые обеспечивают условие инварианта после шага цикла.
После определения всех условий цикла и тела вместе с шагом цикл можно записать на языке высокого уровня.