Е.А. Жоголев - Лекции по технологии программирования (1134164), страница 13

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 13)

В силу произвольности выбора состояния информационной среды теорема доказана.

Примером свойства оператора присваивания может служит пример 9.1.

1. Свойства основных конструкций структурного программирования.

Рассмотрим теперь свойства основных конструкций структурного программирования: следования, разветвления и повторения.

Свойства следования выражает следующая

Теорема 9.3. Пусть P, Q и R - предикаты над информационной средой, а S1 и S2 - обобщенные операторы, обладающие соответственно свойствами

{P}S{Q} и {Q}S2{R}.

Тогда для составного оператора

S1; S2

имеет место свойство

{P} S1; S2 {R} .

Доказательство. Пусть для некоторого состояния информационной среды перед выполнением оператора S1 истинен предикат P. Тогда в силу свойства оператора S1 после его выполнения будет истинен предикат Q. Так как по семантике составного оператора после выполнения оператора S1 будет выполняться оператор S2, то предикат Q будет истинен и перед выполнением оператора S2. Следовательно, после выполнения оператора S2 в силу его свойства будет истинен предикат R, а так как оператор S2 завершает выполнение составного оператора (в соответствии с его семантикой), то предикат R будет истинен и после выполнения данного составного оператора, что и требовалось доказать.

Например, если имеют место свойства (9.2) и (9.3), то имеет

место и свойство

{n<m} n:=n+k; n:=3*n {n<3*(m+k)}.

Свойство разветвления выражает следующая

Теорема 9.4. Пусть P, Q и R - предикаты над информационной средой, а S1 и S2 - обобщенные операторы, обладающие соответственно свойствами

{P,Q} S1{R} и {P,Q} S2 {R}.

Тогда для условного оператора

ЕСЛИ P ТО S1 ИНАЧЕ S2 ВСЕ ЕСЛИ

имеет место свойство

{Q} ЕСЛИ P ТО S1 ИНАЧЕ S2 ВСЕ ЕСЛИ {R} .

Доказательство. Пусть для некоторого состояния информационной среды перед выполнением условного оператора истинен предикат Q. Если при этом будет истинен также и предикат P, то выполнение условного оператора в соответствии с его семантикой сводится к выполнению оператора S1. В силу же свойства оператора S1 после его выполнения (а в этом случае - и после выполнения условного оператора) будет истинен предикат R. Если же перед выполнением условного оператора предикат P будет ложен (а Q, по-прежнему, истинен), то выполнение условного оператора в соответствии с его семантикой сводится к выполнению оператора S2. В силу же свойства оператора S2 после его выполнения (а в этом случае - и после выполнения условного оператора) будет истинен предикат R. Тем самым теорема полностью доказана.

Прежде чем переходить к свойству конструкции повторения следует отметить полезную для дальнейшего

Теорему 9.5. Пусть P, Q, P1 и Q1 - предикаты над информационной средой, для которых справедливы импликации

P1=>P и Q=>Q1,

и пусть для оператора S имеет место свойство {P}S{Q}.Тогда имеет место свойство {P1}S{Q1} .

Эту теорему называют еще теоремой об ослаблении свойств.

Доказательство. Пусть для некоторого состояния информационной среды перед выполнением оператора S истинен предикат P1. Тогда будет истинен и предикат P (в силу импликации P1=>P). Следовательно, в силу свойства оператора S после его выполнения будет истинен предикат Q, а значит и предикат Q1 (в силу импликации Q=>Q1). Тем самым теорема доказана.

Свойство повторения выражает следующая

Теорема 9.6. Пусть I, P, Q и R - предикаты над информационной средой, для которых справедливы импликации

P=>I и (I,Q)=>R ,

и пусть S - обобщенный оператор, обладающий свойством {I}S{I}.

Тогда для оператора цикла

ПОКА Q ДЕЛАТЬ S ВСЕ ПОКА

имеет место свойство

{P} ПОКА Q ДЕЛАТЬ S ВСЕ ПОКА {R} .

Предикат I называют инвариантом оператора цикла.

Доказательство. Для доказательства этой теоремы достаточно доказать свойство

{I} ПОКА Q ДЕЛАТЬ S ВСЕ ПОКА {I,Q}

(по теореме 9.5 на основании имеющихся в условиях данной теоремы импликаций). Пусть для некоторого состояния информационной среды перед выполнением оператора цикла истинен предикат I. Если при этом предикат Q будет ложен, то оператора цикла будет эквивалентен пустому оператору (в соответствии с его семантикой) и в силу теоремы 9.1 после выполнения оператора цикла будет справедливо утверждение (I,Q). Если же перед выполнением оператора цикла предикат Q будет истинен, то оператор цикла в соответствии со своей семантикой может быть представлен в виде составного оператора

S; ПОКА Q ДЕЛАТЬ S ВСЕ ПОКА

В силу свойства оператора S после его выполнения будет истинен предикат I, и возникает исходная ситуация для доказательства свойства оператора цикла: предикат I истинен перед выполнением оператора цикла, но уже для другого (измененного) состояния информационной среды (для которого предикат Q может быть либо истинен либо ложен). Если выполнение оператора цикла завершается, то применяя метод математической индукции мы за конечное число шагов, придем к ситуации, когда перед его выполнением будет справедливо утверждение (I,Q). А в этом случае, как было доказано выше, это утверждение будет справедливо и после выполнения оператора цикла. Теорема доказана.

Например, для оператора цикла из примера (9.4) имеет место свойство

{n>0, p=1, m=1} ПОКА m /= n ДЕЛАТЬ

m:= m+1; p:= p*m

ВСЕ ПОКА {p= n!}.

Это следует из теоремы 9.6, так как инвариантом этого оператора цикла является предикат p=m! и справедливы импликации

(n>0, p=1, m=1) => p=m! и (p=m!, m=n) => p=n!

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

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

Теорема 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.5. Пример доказательства свойства программы.

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

В качестве примера докажем свойство (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.

Упражнения к лекции 9.

1. Пусть заданы описания

const n= <конкретное целое значение>;

var k, m: integer;

x: array[0..n] of integer;

Доказать свойство программы:

{n>0}

m:= x[1]

k:=1;

ПОКА k<n ДЕЛАТЬ

k:=k+1;

ЕСЛИ x[k]<m ТО

m:=x[k]

ВСЕ ЕСЛИ

ВСЕ ПОКА;

{n>0 & для всех i, 1<= i <= n, min <= x[i]}

Литература к лекции 9.

9.1. С.А. Абрамов. Элементы программирования. - М.: Наука, 1982. С. 85-94.

9.2. М. Зелковец, А. Шоу, Дж. Гэннон. Принципы разработки программного обеспечения. - М.: Мир, 1982. С. 98-105.

Лишь та - ошибка, что не исправляется.

Конфуций

Лекция 10.

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

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

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

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

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

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

10.2. Принципы и виды отладки.

Успех отладки в значительной степени предопределяет рациональная организация тестирования. При отладке отыскиваются и устраняются, в основном, те ошибки, наличие которых в ПС устанавливается при тестировании. Как было уже отмечено, тестирование не может доказать правильность ПС [10.9], в лучшем случае оно может продемонстрировать наличие в нем ошибки. Другими словами, нельзя гарантировать, что тестированием ПС практически выполнимым набором тестов можно установить наличие каждой имеющейся в ПС ошибки. Поэтому возникает две задачи. Первая: подготовить такой набор тестов и применить к ним ПС, чтобы обнаружить в нем по возможности большее число ошибок. Однако чем дольше продолжается процесс тестирования (и отладки в целом), тем большей становится стоимость ПС. Отсюда вторая задача: определить момент окончания отладки ПС (или отдельной его компоненты). Признаком возможности окончания отладки является полнота охвата пропущенными через ПС тестами (т.е. тестами, к которым применено ПС) множества различных ситуаций, возникающих при выполнении программ ПС, и относительно редкое проявление ошибок в ПС на последнем отрезке процесса тестирования. Последнее определяется в соответствии с требуемой степенью надежности ПС, указанной в спецификации его качества.

Для оптимизации набора тестов, т.е. для подготовки такого набора тестов, который позволял бы при заданном их числе (или при заданном интервале времени, отведенном на тестирование) обнаруживать большее число ошибок, необходимо, во-первых, заранее планировать этот набор и, во-вторых, использовать рациональную стратегию планирования (проектирования [10.1]) тестов. Проектирование тестов можно начинать сразу же после завершения этапа внешнего описания ПС. Возможны разные подходы к выработке стратегии проектирования тестов, которые можно условно графически разместить (см. рис. 9.1) между следующими двумя крайними подходами [10.1]. Левый крайний подход заключается в том, что тесты проектируются только на основании изучения спецификаций ПС (внешнего описания, описания архитектуры и спецификации модулей). Строение модулей при этом никак не учитывается, т.е. они рассматриваются как черные ящики. Фактически такой подход требует полного перебора всех наборов входных данных, так как при использовании в качестве тестов только части этих наборов некоторые участки программ ПС могут не работать ни на каком тесте и, значит, содержащиеся в них ошибки не будут проявляться. Однако тестирование ПС полным множеством наборов входных данных практически неосуществимо. Правый крайний подход заключается в том, что тесты проектируются на основании изучения текстов программ с целью протестировать все пути выполнения каждой программ ПС. Если принять во внимание наличие в программах циклов с переменным числом повторений, то различных путей выполнения программ ПС может оказаться также чрезвычайно много, так что их тестирование также будет практически неосуществимо.

Рис. 10.1. Спектр подходов к проектированию тестов.

Характеристики

Список файлов лекций