Вопрос №14 Ограничивающая ф-ция оператора цикла.Примеры №14

Правило 8 (проверка завершимости цикла while B do S). Пусть t = t(X) – целочисленная функция переменных X, удовлетворяющая условиям:

1) t  0;

2) P & B  (t > 0);

3) для любого значения t₀ функции t имеет место св-во

{(P & B) & (0 < t = t₀)} S {0  t < t₀};

тогда выполнение цикла while B do S завершится.

Условие 1 означает, что утверждение t  0 – один из инвариантов цикла. Условие 2 означает, что перед выполнением тела цикла t > 0. Условие 3 означает, что функция t(X) убывает на каждом шаге цикла.

Справедливость правила 8 следует из того, что любая целочисленная убывающая последовательность с положительными элементами конечна.

Функция t(X) называется ограничивающей функцией цикла. В принципе, наличие ограничивающей функции не только доказывает завершимость цикла, но и позволяет оценить число его шагов: оно заведомо не превысит величины t(X₀), где X₀ – начальные значения переменных цикла.

Подбор ограничивающей ф-ции, как и подбор инварианта цикла, требует изобретательности.

Пример.

Пусть дана циклическая программа (для n: Integer):

while n > 1 do

if Odd(n) then n := n + 1 else n := n div 2

Функцию t(n) для n  1 определим следующим образом:

0, если n = 1,

t(n) = 

n  (1)ⁿ, если n > 1.

Проверим условия правила 8. Условия 1 и 2 выполнены, поскольку t(1) = 0, а если n > 1, то n  (1)ⁿ  n – 1 > 0. Условие 3 проверим отдельно для четного и нечетного n. Пусть n – четно. Если n > 4, то t(n div 2)  n div 2 + 1 < t(n) = t₀. При n = 4: t(n div 2) = t(2) = 1 < t(n) = t₀ = 3. При n = 2: t(n div 2) = t(1) = 0 < t(n) = t₀ = 1. Пусть теперь n – нечетно. Тогда t(n) = t₀ = n + 1, а t(n + 1) = t = n, т. е. t < t₀.

Отметим, что сама по себе функция t(n) не монотонна: t(1) = 0, t(2) = 1,t(3) = 4, t(4) = 3, t(5) = 6, t(6) = 5, t(7) = 8, t(8) = 7, t(9) = 10, t(10) = 9, t(11) = 12, t(12) = 11, ... . Она монотонно изменяется лишь на последовательности аргументов, порождаемой при работе цикла. Пусть, например, начальное значение n = 11, тогда при выполнении цикла порождается последовательность значений n = 11, 12, 6, 3, 4, 2, 1 и на этой последовательности функция t(n) строго убывает: t(n) = 12, 11, 5, 4, 3, 1, 0.

До сих пор не доказана и не опровергнута завершимость цикла

while n > 1 do 

if Odd(n) then n := 3*n + 1 else  n := n div 2

Пример незавершающегося цикла (для n > 1):

while n > 1 do 

if Odd(n) then n := n + 1 else n := n div 2 + 1

Действительно, тело цикла обладает легко проверяемым свойством {n > 1} S {n > 1}, поэтому условие окончания цикла not (n > 1) не может быть выполнено.

Билет№15. Теорема о цикле, его инварианте и ограничивающей функции №15

Теорема (о цикле while-do, его инварианте и ограничивающей функции). Рассмотрим цикл while B do S. Предположим, что предикат P удовлетворяет условию

1) {P & B} S {P}.

Далее пусть t – целочисленная функция от переменных программы, удовлетворяющая следующим условиям (t1 – переменная целого типа):

2) P & B  (t > 0);

3) {P & B} begin t1 := t;S end {0  t < t1}.

Тогда имеет место свойство цикла {P} while B do S {P & not B} и цикл завершится.

Аннотирование цикла и понимание аннотаций.

Цикл рекомендуется оформлять следующим образом:

{Q}

{inv P: инвариант }

{bound t : ограничивающая функция }

while B do

begin

S

end {while};

{R}

Здесь Q – предусловие, а R  постусловие цикла, и выполняются соотношения Q  P, not B & P  R.

Список условий для проверки (аннотированного) цикла:

1) показать, что P – истинно до выполнения цикла, т. е. Q  P;

2) показать, что тело цикла имеет свойство {B & P} S {P}, т. е. P – инвариант;

3) показать, что not B & P  R;

4) показать, что P & B  (t > 0);

5) показать, что {P & B} begin t1 := t; S end {0  t < t1}, т. е. t уменьшается на каждом шаге цикла.

Рассмотрим пример:

var n, i: Integer; { n > 0 }

i := 1;

{inv P: (0 < i  n)} {bound t: ni}

while (2*i) <= n do i := 2*i ;

{post: ( 0<i  n < 2*i)}

Проверим 5 указанных ранее условий.

1) Очевидно {(n > 0) & (i = 1)}  inv.

2) Проверим свойство {B & inv} i := 2*i {inv}. В соответствии с правилом вывода оператора присваивания имеем: {предусловие} i := 2*i {0<i  n}. Слабейшее предусловие есть {0 < 2*i  n}. Очевидно, что оно следует из (B & inv), которое в данном случае есть {(2*i  n) & (0 < i  n)}.

3) Утверждение not B есть 2*i > n. Отсюда очевидно, что (not B & inv)  post.

4) t = n  i > 0 при 0 < 2*i  n.

5) Проверим свойство {0 < 2*i  n} t1:= n  i; i := 2*i {0  t < t1}.Действительно, wp(t1 := n  i;  i:= 2*i  0  n  i < t1)  (0  n  2*i < n  i) и (0 < 2*i  n)  wp (...).