С циклом связано еще одно важное понятие - варианта цикла, используемое для доказательства завершаемости цикла. Определение 5 (варианта цикла): целочисленное неотрицательное выражение Var(x, z) называется вариантом цикла, если выполняется следующая триада: {(Var(x,z)= n) & B} S(x,z){(Var(x,z)= m) & (m < n)} Содержательно это означает, что каждое выполнение тела цикла приводит к уменьшению значения его варианта. После конечного числа шагов вариант достигает своей нижней границы, и цикл завершается. Простейшим примером варианта цикла является выражение n-i для цикла: for(i=1; i<=n; i++) S(x, z); Пользоваться инвариантами и вариантами цикла нужно не только и не столько для того, чтобы проводить формальное доказательство корректности циклов. Они способствуют написанию корректных циклов. Правило корректного программирования гласит: "При написании каждого цикла программист должен определить его походящий инвариант и вариант". Задание предусловий, постусловий, вариантов и инвариантов циклов является такой же частью процесса разработки корректного метода, как и написание самого кода. Рекурсия является одним из наиболее мощных средств в арсенале программиста. Рекурсивные структуры данных и рекурсивные методы широко используются при построении программных систем. Рекурсивные методы, как правило, наиболее всего удобны при работе с рекурсивными структурами данных - списками, деревьями. Рекурсивные методы обхода деревьев служат классическим примером. Определение 6 (рекурсивного метода): метод P (процедура или функция) называется рекурсивным, если при выполнении тела метода происходит вызов метода P. Рекурсия может быть прямой, если вызов P происходит непосредственно в теле метода P. Рекурсия может быть косвенной, если в теле P вызывается метод Q (эта цепочка может быть продолжена), в теле которого вызывается метод P. Определения методов P и Q взаимно рекурсивны, если в теле метода Q |