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

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

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

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

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

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

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

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

Однако ошибки могутбыть и тогда, когда она делает, и что от нее не требуется.Подводя итог, можно сказать, что тестирование представляется деструктивным процессом попыток обнаружения ошибок в программе (наличие которых предполагается). Набор тестов, способствующий обнаружению ошибки, считается удач-88ным. Естественно, в конечном счете, каждый с помощью тестирования хочет добиться определенной степени уверенности втом, что его программа соответствует своему назначению и неделает того, для чего она не предназначена, но лучшим средством для достижения этой цели является непосредственныйпоиск ошибок. Допустим, кто-то обращается к вам с заявлением: «Моя программа великолепна» (т.е.