Основы программирования на C#


Инварианты и варианты цикла - часть 2


Это означает, что из истинности инварианта и условия завершения цикла следует требуемое постусловие.

Определение 4 (подходящего инварианта): предикат RealInv, удовлетворяющий условиям (*), (**), (***) называется подходящим инвариантом цикла.

С циклом связано еще одно важное понятие - варианта цикла, используемое для доказательства завершаемости цикла.

Определение 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);

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




Начало  Назад  Вперед