Студопедия
Случайная страница | ТОМ-1 | ТОМ-2 | ТОМ-3
АрхитектураБиологияГеографияДругоеИностранные языки
ИнформатикаИсторияКультураЛитератураМатематика
МедицинаМеханикаОбразованиеОхрана трудаПедагогика
ПолитикаПравоПрограммированиеПсихологияРелигия
СоциологияСпортСтроительствоФизикаФилософия
ФинансыХимияЭкологияЭкономикаЭлектроника

Завершимость выполнения программы.

Обоснования программ. Формализация свойств программ. | Принципы и виды отладки. | Заповеди отладки. | Автономная отладка модуля. | Комплексная отладка программного средства. | Обеспечение завершенности программного средства. | Обеспечение устойчивости программного средства. | Обеспечение защищенности программных средств. | Общая характеристика процесса обеспечения качества программного средства. | Обеспечение эффективности программного средства. |


Читайте также:
  1. I. Предметы, необходимые для выполнения ритуала
  2. аблон для выполнения задания по практикуму 1.
  3. адачи лабораторной работы и последовательность ее выполнения.
  4. Алгоритм выполнения трудовых действий при приемке риса по количеству и качеству
  5. Анализ, ошибки и оценки выполнения техники движений
  6. атериал для выполнения задания № 10
  7. атериал для выполнения задания № 13

Одно из свойств программы, которое нас может интересовать, чтобы избежать возможных ошибок в ПС, является ее завершимость, т.е. отсутствие в ней зацикливания при тех или иных исходных данных. В рассмотренных нами структурированных программах источником зацикливания может быть только конструкция повторения. Поэтому для доказательства завершимости программы достаточно уметь доказывать завершимость оператора цикла. Для этого полезна следующая Теорема 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) раз, т.е. этот оператор цикла завершается.

 


Дата добавления: 2015-08-02; просмотров: 67 | Нарушение авторских прав


<== предыдущая страница | следующая страница ==>
Свойства основных конструкций структурного программирования.| Пример доказательства свойства программы

mybiblioteka.su - 2015-2024 год. (0.005 сек.)