Помощничек
Главная | Обратная связь


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

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



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

Теорема 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.

 

 

ТЕСТИРОВАНИЕ И ОТЛАДКА ПРОГРАММНОГО СРЕДСТВА

Основные понятия. Стратегия проектирования тестов. Заповеди отладки. Автономная отладка и тестирование программного модуля. Комплексная отладка и тестирование программного средства.

Основные понятия.

Отладка ПС - это деятельность, направленная на обнаружение и исправление ошибок в ПС с использованием процессов выполнения его программ. Тестирование ПС - это процесс выполнения его программ на некотором наборе данных, для которого заранее известен результат применения или известны правила поведения этих программ. Указанный набор данных называется тестовым или просто тестом. Таким образом, отладку можно представить в виде многократного повторения трех процессов: тестирования, в результате которого может быть констатировано наличие в ПС ошибки, поиска места ошибки в программах и документации ПС и редактирования программ и документации с целью устранения обнаруженной ошибки. Другими словами:

Отладка = Тестирование + Поиск ошибок + Редактирование.

В зарубежной литературе отладку часто понимают [10.1-10.3] только как процесс поиска и исправления ошибок (без тестирования), факт наличия которых устанавливается при тестировании. Иногда тестирование и отладку считают синонимами [10.4,10.5]. В нашей стране в понятие отладки обычно включают и тестирование [10.6 -10.8], поэтому мы будем следовать сложившейся традиции. Впрочем совместное рассмотрение в данной лекции этих процессов делает указанное разночтение не столь существенным. Следует однако отметить, что тестирование используется и как часть процесса аттестации ПС (см. лекцию 14).

 




Поиск по сайту:

©2015-2020 studopedya.ru Все права принадлежат авторам размещенных материалов.