Калайда В.Т., Романенко В.В. Технология разработки программного обеспечения (1015641), страница 12

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

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

Массивы. Структуры. Списки. Очереди. Стеки. Множества. Графы. Деревья.9. Абстрактные конструкции.10. Фиксированные данные абстрактного типа.11. Размещение указателей.12. Защита данных от несанкционированного доступа.785 ПРАВИЛЬНОСТЬ ПРОГРАММОдним из важных методов повышения эффективностипроектирования программ является верификация программ илиматематическое доказательство того, что программа работаетправильно.

Для доказательства правильности программ используется аксиоматический подход, при котором применяется теория перечисления предикатов. Предполагается, что каждый оператор в программе выполняет заранее определенные действия,зависящие только от синтаксиса языка. Для двух предикатов Pи Q и оператора S необходимо определить, истинно ли выражение:«Если P истинно и если выполняется оператор S, то Q истинно».Предикат P является спецификацией правильного выполнения оператора S, а предикат Q будет истинным после выполнения оператора S и является спецификацией следующего за Sоператора.Если это утверждение распространить на все операторыпрограммы и если P является спецификацией первого оператора, а Q истинно после окончания программы, то будет доказанаправильность всей программы относительно предикатов P и Q.Эту конструкцию можно записать в следующем виде:{ P} S { Q} ,где P называется предусловием истинности Q после выполнения программы S.Доказательство правильности программы заключается вопределении, является ли выражение {P}S{Q} истинным относительно входных спецификаций P, выходных спецификаций Q иоператоров S программы.

Если {P}S{Q} истинно, то это означает,что доказана правильность программы S относительно P и Q.5.1 АксиомыДля целей доказательства правильности программ к правилам исчисления предикатов следует добавить правила, необходимые для выполнения последовательности операторов программы. Эти правила, называемые правилами следствия, формулируются следующим образом:791) если {P}S{Q} и Q  R, то {P}S{R};2) если {Q}S{R} и P  Q, то {P}S{R}.Первое правило заключается в следующем: «Если P —предусловие для Q и если Q  R является теоремой исчисленияпредикатов, то P — предусловие для R».

Таким образом, если Pистинно и выполняется S, то R (так же, как и Q) истинно.Второе правило следствия аналогично данному. Эти правила следствия можно представить в более формальном виде:числитель выражения является посылкой, а знаменатель — заключением:1)2){ P} S { Q} , Q{ P} S { R}{ Q} S { R} , P{ P} S { R}RQ;.Правила следствия используются для доказательствасложных элементов программы. Пусть программа представленав виде структуры (рис. 5.1), где Si — операторы, а Pi — предикаты, соответствующие дугам.S1НачалоP1S2P2КонецP3Рис. 5.1 — Структура программыПредположим, что доказаны следующие утверждения:{P1}S1{P1'} и {P2}S2{P2'} для некоторых предикатов P1' и P2'.Если можно доказать, что P1'  P2 и P2'  P3, то, используяправила следствия, можно доказать, что {P1}S1;S2{P3} истинно.Следует определить, какие операторы программы являются правильными.

Предполагается, что программа состоит только из последовательности операторов присвоения и операторовif и do while.Так как только оператор присвоения может изменять значение переменных, то для определения правильности оператораприсвоения нужно добавить только одну аксиому, она называ-80ется аксиомой присвоения и формулируется следующим образом:x = expr, P ( x ){ P ( expr ) } x = expr { P ( x ) }.В соответствии с этой аксиомой устанавливается, чтоесли P — утверждение, содержащее переменную x, истинно, тоP должно быть истинно и до выполнения оператора присвоения, если x изменяется expr.Например, если P(x) является предикатом x > 0 и x = x + 1— оператор присвоения, то P(x + 1) является предикатомx + 1 > 0 или x > –1.По правилам следствия, если можно доказать, что Q P(x + 1) для некоторого предиката Q, то справедливо утверждение {Q}x = x + 1{x > 0} и предикат является предусловием для P.Осталось определить правильные управляющие структуры.

Введем следующие аксиомы.Аксиома следования:{ P} S1 { Q} ,{ Q} S2 { R} .{ P} S1; S2 { R}Два оператора программы могут быть объединены. Еслипосле выполнения S1 предикат Q остается истинным и Q естьпредусловие для оператора S2, то P является предусловием дляоператоров S1; S2.Аксиома цикла:{ P & B} S { P}{ P} do while ( B ) ; and ;{B & P}.Утверждается, что если истинность P не изменяется оператором S (т.е. является инвариантом), то P инвариантно относительно цикла, содержащего S.

Кроме того, при выходе из цикла значение выражения B ложно.Аксиома выбора:{ P & B} S1 { Q} ,{ P & B} S2 { Q} ;{ P} if B then S1; else S2 { Q}{ P & B} S1, P & B Q .б){ P} if B then S1 { Q}а)81Эти аксиомы устанавливают простые соотношения дляоператора if.5.2 Правила преобразования данныхКоммутативность:x + y = y + x;x y = y x.Ассоциативность:( x + y) + z = x + ( y + z) ;( x y) z = x ( y z) .Дистрибутивность:x( y + z) = ( xВычитание:Обработка констант:y) + ( x z) .x  y + y = x.x + 0 = x;x 0 = 0;x 1 = x.5.3 Доказательства правильности программИспользуя приведенные выше правила и аксиомы, можноосуществлять доказательство правильности программ. Рассмотрим следующую программу:1. MULTIPLY (R,A,B);2. declare X;3.

declare R;/*R=A*B*/4. declare A,B; /*B0*/5. R=0;6. X=B;7. do while (X0);8. R=R+A;9. X=X-1;10. end;11. end MULTIPLY;82Входным утверждением является предикат B ≥ 0, выходное утверждение R = A×B.Общая схема доказательства правильности программы:Строка 5. {0 = 0 & B ≥ 0} R = 0 {R = 0 & B ≥ 0} по аксиоме присваивания; {B ≥ 0} R = 0 {R = 0 & B ≥ 0} по правилу следствия всвязи с тем, что истинны следующие утверждения:истинно  0 = 0;B ≥ 0  (B ≥ 0 & истинно).Строка 6. {B = B & R = 0 & B ≥ 0} X = B {X = B & R = 0 & B ≥ 0}по аксиоме присвоения; {R = 0 & B ≥ 0} X = B {X = B & R = 0 & B ≥ 0} по аксиоме следования; {B ≥ 0} R = 0; X = B {X = B & R = 0 & B ≥ 0} по аксиомеследования.Таким образом, показано, что если B ≥ 0 (входное предусловие), то после выполнения строки 6 выражение {X = B & R == 0 & B ≥ 0} истинно.Строки 7–10.Необходим инвариант для предиката P цикла do while.Этот инвариант должен описывать работу, выполняемую циклом.

В нашем случае цикл вычисляет произведение; таким образом, инвариантом может быть R = A×(B – X). В соответствии саксиомой цикла, если можно показать, что это выражение инвариантно относительно цикла и что оно истинно, когда цикл заканчивается, то возникает следующая ситуация: R = A×(B – X) — инвариант цикла; X = 0 — выражение внутри цикла ложно.Таким образом, если выражение R = A×(B – X) & (X = 0)истинно, то истинно и выражение R = A×(B – 0) & (X = 0), а этоприводит к истинности соотношения R = A×B, что и требовалось доказать. Следовательно, для того, чтобы завершить доказательство, нужно, чтобы выражение R = A×(B – X) в строке 7было истинно и оно является инвариантом цикла.Доказательство того, что указанное выражение есть инвариант цикла, проводится следующим образом:83Строка 8. {R + A = A×B – A×X + A} R = R + A {R = A×B – A×X + A}по аксиоме присвоения; {R = A×B – A×X} R = R + A {R = A×B – A×X + A} по правилам целочисленной арифметики; {R = A×(B – X)} R = R + A {R = A×B – A×X + A} по правилам дистрибутивности.Строка 9. {R = A×(B – (X – 1))} X = X – 1 {R = A×(B – X)} по аксиоме присвоения; {R = A×B – A×(X – 1)} X = X – 1 {R = A×(B – X)} по правилам целочисленной арифметики.Объединение строк 8 и 9 в соответствии с аксиомой следования дает выражение {R = A×(B – X)} R = R + A; X = X – 1{R= = A×(B – X)}, которое является желаемым инвариантом соотношения.Теперь следует показать, что инвариантное выражение встроке 7 истинно, а это эквивалентно доказательству с помощьюправил следования следующей теоремы: X = B & R = 0 & B ≥ 0 истинно в строке 6  R = A×(B – X).Остановимся на нескольких важных моментах в связи сдоказательством правильности программ. Доказательства длинны и сложны даже для простойпрограммы. Если оперировать нецелочисленными данными, тоформулировка аксиом становится затруднительной.Операции со строками, плавающей точкой, доступ кбазам данных вызывают серьезные осложнения при аксиоматическом подходе. Даже для относительно простого случая — использования целочисленных данных — существуют трудности.

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

Кроме того, предусловия являются базой для разработки тестов программ. Все предусловия могут быть закодированы как операторы if и выполняться как часть теста.Контрольные вопросы1.2.3.4.5.6.7.Правильность программ.Правила следствия.Аксиома присвоения.Аксиома следования.Аксиома цикла.Аксиома выбора.Правила целочисленной арифметики — коммутативность, ассоциативность, дистрибутивность, вычитание,обработка констант.8. Доказательство правильности программ.856 ТЕСТИРОВАНИЕ6.1 Психология и экономика тестированияпрограммТестирование как объект изучения может рассматриваться с различных, чисто технических, точек зрения. Однако наиболее важными при изучении тестирования представляются вопросы его экономики и психологии разработчика.

Иными словами, достоверность тестирования программы, в первую очередь, определяется тем, кто будет ее тестировать и каков его образ мышления, и уже затем определенными технологическимиаспектами. Поэтому, прежде чем перейти к техническимпроблемам, мы остановимся на этих вопросах.Поначалу может показаться тривиальным жизненно важный вопрос определения термина «тестирование». Необходимость обсуждения этого термина связана с тем, чтобольшинство специалистов используют его неверно, а это, всвою очередь, приводит к плохому тестированию. Таковы,например, следующие определения: «Тестирование представляет собой процесс, демонстрирующий отсутствие ошибок впрограмме», «цель тестирования — показать, что программакорректно исполняет предусмотренные функции», «тестирование — это процесс, позволяющий убедиться в том, что программа выполняет свое назначение».Эти определения описывают нечто противоположноетому, что следует понимать под тестированием, поэтому ониневерны.

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

Дело втом, что верный выбор цели дает важный психологический эффект, поскольку для человеческого сознания характерна целевая направленность. Если поставить целью демонстрацию отсутствия ошибок, то мы подсознательно будем стремиться кэтой цели, выбирая тестовые данные, на которых вероятностьпоявления ошибки мала. В то же время, если нашей задачейстанет обнаружение ошибок, то создаваемый нами тест будетобладать большей вероятностью обнаружения ошибки. Такойподход заметнее повысит качество программы, чем первый.Из приведенного определения тестирования вытекаетнесколько следствий. Например, одно из них состоит в том, чтотестирование — процесс деструктивный (т.е. обратный созидательному, конструктивному). Именно этим и объясняется, почему многие считают его трудным. Большинство людей склоннык конструктивному процессу созидания объектов и в меньшейстепени — к деструктивному процессу разделения на части. Изопределения следует также то, как нужно строить набор тестовых данных и кто должен (а кто не должен) тестировать даннуюпрограмму.Для усиления определения тестирования проанализируемдва понятия «удачный» и «неудачный» и, в частности, их использование руководителями проектов при оценке результатовтестирования.

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

Список файлов книги