Анализ завершенности последовательных программ

Особенность свойства завершенности программ состоит в том, что оно не зависит от постусловия программы, и для заданной программы полностью определяется предусловием. В общем случае формальный анализ свойства завершенности представляет весьма сложную проблему.

Имеются по меньшей мере две причины, по которым программа с заданным предусловием P может не завершиться:

· обращение к частично определенной функции со значением аргументов вне области определения;

· зацикливание.

Первая причина может приводить к аварийному завершению даже нециклических программ (например, при делении на нуль). Вторая причина присуща программам с итеративными циклами.

Ограничимся рассмотрением методов анализа завершения циклических вычислений без учета других возможных причин незавершения, т.е. предполагается, что любой нециклический оператор завершается и передает управление на его выход.

Наибольшее распространение получили два метода логического анализа завершения циклических вычислений:

· метод Флойда;

· метод счетчиков.