Основы программирования на 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);

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

on_load_lecture()

Дальше »

  Если Вы заметили ошибку - сообщите нам.  

Страницы:

« |

1

|

2

|

3

|

4

|

5

|

вопросы | »

|

учебники

|

для печати и PDA

Курсы | Учебные программы | Учебники | Новости | Форум | Помощь



Телефон: +7 (495) 253-9312, 253-9313, факс: +7 (495) 253-9310, email: info@intuit.ru

© 2003-2007, INTUIT.ru::Интернет-Университет Информационных Технологий - дистанционное образование




Содержание  Назад  Вперед