Завершимость выполнения программы.
Одно из свойств программы, которое нас может интересовать, чтобы избежать возможных ошибок в ПС, является ее завершимость, т.е. отсутствие в ней зацикливания при тех или иных исходных данных. В рассмотренных нами структурированных программах источником зацикливания может быть только конструкция повторения. Поэтому для доказательства завершимости программы достаточно уметь доказывать завершимость оператора цикла. Для этого полезна следующая
Теорема 9.7. Пусть F - целочисленная функция, зависящая от состояния информационной среды и удовлетворяющая следующим условиям:
(1) если для данного состояния информационной среды истинен предикат Q, то ее значение положительно;
(2) она убывает при изменении состояния информационной среды в результате выполнения оператора S.
Тогда выполнение оператора цикла
ПОКА Q ДЕЛАТЬ S ВСЕ ПОКА
завершается.
Доказательство. Пусть is - состояние информационной среды перед выполнением оператора цикла и пусть F(is)=k. Если предикат Q(is) ложен, то выполнение оператора цикла завершается. Если же Q(is) истинен, то по условию теоремы k>0. В этом случае будет выполняться оператор S один или более раз. После каждого выполнения оператора S по условию теоремы значение функции F уменьшается, а так как перед выполнением оператора S предикат Q должен быть истинен (по семантике оператора цикла), то значение функции F в этот момент должно быть положительно (по условию теоремы). Поэтому в силу целочисленности функции F оператор S в этом циклене может выполняться более k раз. Теорема доказана.
|
|
Например, для рассмотренного выше примера оператора циклаусловиям теоремы 9.7 удовлетворяет функция f(n, m)= n-m. Так как перед выполнением оператора цикла m=1, то тело этого цикла будет выполняться (n-1) раз, т.е. этот оператор цикла завершается.
На основании доказанных правил верификации программ можно доказывать свойства программ, состоящих из операторов присваивания и пустых операторов и использующих три основные композиции структурного программирования. Для этого анализируя структуру программы и используя заданные ее пред- и постусловия необходимо на каждом шаге анализа применять подходящее правило верификации. В случае применения композиции повторения потребуется подобрать подходящий инвариант цикла.
В качестве примера докажем свойство (9.4). Это доказательство будет состоять из следующих шагов.
(Шаг 1). n>0 => (n>0, p - любое, m - любое).
(Шаг 2). Имеет место
{n>0, p - любое, m - любое} p:=1 {n>0, p=1, m - любое}.
-- По теореме 9.2.
(Шаг 3). Имеет место
{n>0, p=1, m - любое} m:=1 {n>0, p=1, m=1}.
-- По теореме 9.2.
|
|
(Шаг 4). Имеет место
{n>0, p - любое, m - любое} p:=1; m:=1 {n>0, p=1, m=1}.
-- По теореме 9.3 в силу результатов шагов 2 и 3.
Докажем, что предикат p=m! является инвариантом цикла, т.е. {p=m!} m:=m+1; p:=p*m {p=m!}.
(Шаг 5). Имеет место {p=m!} m:=m+1 {p=(m-1)!}.
-- По теореме 9.2, если представить предусловие в виде {p=((m+1)-1)!}.
(Шаг 6). Имеет место {p=(m-1)!} p:=p*m {p=m!}.
-- По теореме 9.2, если представить предусловие в виде {p*m=m!}.
(Шаг 7). Имеет место инвариант цикл
{p=m!} m:=m+1; p:=p*m {p=m!}.
-- По теореме 9.3 в силу результатов шагов 5 и 6.
(Шаг 8). Имеет место
{n>0, p=1, m=1} ПОКА m /= n ДЕЛАТЬ
m:= m+1; p:= p*m
ВСЕ ПОКА {p= n!}.
-- По теореме 9.6 в силу результата шага 7 и имея в виду, что (n>0, p=1, m= 1)=>p=m!; (p=m!, m=n)=>p=n!.
(Шаг 9). Имеет место
{n>0, p - любое, m - любое} p:=1; m:=1;
ПОКА m /= n ДЕЛАТЬ
m:= m+1; p:= p*m
ВСЕ ПОКА {p= n!}.
-- По теореме 9.3 в силу результатов шагов 3 и 8.
(Шаг 10). Имеет место свойство (9.4) по теореме 9.5 в силу результатов шагов 1 и 9.